%
%  $Description: Sample bibliography$
%
%  $Author: zaraket $
%  $Date: 2007/09/11 00:29:51 $
%  $Revision: 1.17 $
%

@string{iccd = "International Conference on Computer Design"}
@string{erl = "Electronics Research Lab"}
@string{fmsd = "Journal of Formal Methods in System Design"}

@String{PROC = "Proceedings of the "}
@string{iscas = "International Symposium on Circuits and Systems"}

@String{DAC = "Design Automation Conference"}
@String{DAC01 = DAC }
@String{SOSP = "ACM Symposium on Operating Systems Principles"}
@String{SOSP99 = PROC # "17th " # SOSP }
@String{MIT-P = "MIT Press, Cambridge, MA"}
@String{NAI = "National Conference on Artificial Intelligence"}
@String{NAI97 = PROC # NAI}
@string{cav = "Computer Aided Verification"}
@String{date = "Design Automation and Test in Europe"};
@string{ieeetc = "IEEE Transactions on Computers"}

@misc{blind,
title  = "{Omitted for Blind Review.}",
}

@INPROCEEDINGS{tcas_impl, 
    author={Hutchins, M. and Foster, H. and Goradia, T. and Ostrand, T.}, 
    journal={International Conference on Software Engineering}, 
    title={Experiments on the effectiveness of dataflow- and control-flow-based test adequacy criteria}, 
    year={1994}, 
    month={may.}, 
    volume={}, 
    number={}, 
}

@inbook{amannBook,
    author =  "Paul Ammann and Jeff Offutt",
    year  =   "2008",
    title =   "Introduction to Software Testing",
    publisher = "Cambridge University Press"
}


@InBook{jackson:_separ_concer_requir_analy,
  author = 	 {Daniel Jackson and Michael Jackson},
  title = 	 {Separating Concerns in Requirements Analysis: An Example},
  publisher = 	 {Springer-Verlag},
}

@article{ErnstPGMPTX2007,
    author = {Michael D. Ernst and Jeff H. Perkins and Philip J. Guo and
        Stephen McCamant and Carlos Pacheco and Matthew S. Tschantz and
            Chen Xiao},
    title = {The {Daikon} system for dynamic detection of likely invariants},
    journal = {Science of Computer Programming},
    volume = {69},
    number = {1--3},
    pages = {35--45},
    month = {December},
    year = {2007}
}

@inproceedings{wangStableVhdlHol91,
  author = "Xinning Wang and Edward P. Stabler",
  title = {Formalization of VHDL Synthesis Procedure in Higher-Order Logic},
  booktitle = {Proceedings of International Tutorial and Workshop on the HOL Theorem Proving System and its Applications},
  month =August,
  year =1991,
}
%pages = {106,119},
%ACM/IEEE, IEEE Computer Society Press

@inproceedings{FuYuMalik2005,
  author = "Zhaohui Fu and Yinlei Yu and Sharad Malik",
  title = {Considering Circuit Observability Don't Cares In CNF Satisfiability},
  booktitle = {Proceedings of Design, Automation and Test in Europe},
  pages = {1108-1113},
  month =March,
  year =2005,
}

@inproceedings{ZhuKu06SATSweepODC,
  author = "Qi Zhu and Nathan Kitchen and Andreas Kuelhman and Alberto  Sangiovanni-Vincentelli",
  title = {SAT Sweeping with Local Observability DontCares},
  booktitle = DAC,
  month = {July},
  year = {2006},
}


@inproceedings{clark05rtlPredicateAbs,
  author = "Himanshu Jain and Daniel Kroening and Natasha Sharygina and Edmund Clarke",
  title = {Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog},
  booktitle = DAC,
  month = {June},
  year = {2005},
}

@inproceedings{Andraus04abstVerif,
   author = {Zaher Andraus and Karem Sakallah},
   title = {Automatic Abstraction and Verification of Verilog Models},
   booktitle = DAC,
   month={June},
   year = {2004},
}

@phdthesis{azizPhd96,
  author={A. Aziz},
  title={Formal Methods in VLSI System Design},
  year="1996",
  school="University of California, Berkley",
}

@inproceedings{clarkCVerilog,
    author = {Edmund Clarke and Daniel Kroening and Karen Yorav},
    title = {Behavioral consistency of C and verilog programs using bounded model checking},
    booktitle = DAC,
    year = {2003},
}

@article{zhu1997,
   author = {H. Zhu and P. A. V. Hall and J.H.R. May},
   title = {Software unit test coverage and adequacy},
   journal = {ACM Computer Surveys},
   year = {1997},
}

@inproceedings{Cadar06exe,
   author = {Cristian Cadar and Paul Twohey and Vijay Ganesh and Dawson Engler},
   title = {EXE: A System for Automatically Generating Inputs of Death Using Symbolic Execution},
   booktitle = {The 13th ACM Conference on Computer and Communications Security (CCS)},
   year = {2006},
   month = {November},
}

@inproceedings{godefroit05dart,
   author = {Nils Godefroid and Sen Patrice and Koushik  Klarlund},
   booktitle = {ACM SIGPLAN conference on Programming language design and implementation},
   month = {June},
  publisher = {ACM Press},
   title = {DART: directed automated random testing},
   year = {2005},
}

@inproceedings{cuteSen2005,
   author = {K. Sen and D. Marinov and G. Agha},
   title = {CUTE: a concolic unit testing engine for C},
   booktitle = {10th European software engineering conference},
   year = {2005},
   location = {Lisbon, Portugal},
}

@inbook{williams05pathcrawler,
   author = {N. Williams and B. Marre and P. Mouy and M. Roger},
   booktitle = {Dependable Computing - EDCC},
   month = {March},
   title = {PathCrawler: Automatic Generation of Path Tests by Combining Static and Dynamic Analysis},
   year = {2005}
}


@inproceedings{xu06data,
   author = {Z. Xu and J. Zhang},
   title = {A Test Data Generation Tool for Unit Testing of C Programs},
   booktitle = {The Sixth International Conference on Quality Software},
   year = {2006},
}


@inproceedings{yang04,
   author = {J. Yang and D. Evans},
   title = {Dynamically inferring temporal properties},
   booktitle = {Workshop on Program analysis for software tools and engineering},
   year = {2004},
}

inproceedings{fine03coverage,
  author = "S. Fine and A. Ziv",
  title = "Coverage directed test generation for functional verification using bayesian networks",
  booktitle = DAC,
  year = {2003},
}

@inproceedings{majumdar07concolic,
 author = {Rupak Majumdar and Koushik Sen},
 title = {Hybrid Concolic Testing},
 booktitle = {International Conference on Software Engineering},
 year = {2007},
}

@inproceedings{nistReport2002,
  title={The economic impacts of inadequate infrastructure for software testing},
  booktitle={National Institute of Standards and Technology, Planning report 02-3},
  year={2002},
  month={May},
}

@inproceedings{masri2009,
    author={W. Masri},
    title={Fault Localization Based on Information Flow Coverage},
    booktitle={Software Testing, Verification and Reliability (Wiley), (to appear)},
    year={2009},
}

@inproceedings{chiodo2002synthesis,
 author = {Massimiliano Chiodo},
 title = {Optimization and synthesis for complex reactive embedded systems by incremental collapsing},
 booktitle = {International symposium on Hardware/software codesign},
 year = {2002},
}

@inproceedings{ chiodo93synthesis,
    author = "{M. Chiodo} and {P. Giusto} and {H. Hsieh} and {A. Jurecska} and {L. Lavango} and {A. Sangiovanni-Vincentelli}",
    title = "Synthesis of Mixed Software-Hardware Implementation from {CFSM} Specifications",
    booktitle = "International Workshop on Hardware-Software Codesign",
    year = "1993",
}

@Book{HaTsLogicSynthesis2003,
  editor= "Soha Hassoun abd Tsutomu Sasao",
  title = "Logic Synthesis and Verification",
  publisher = "Kluwer Academic Publishers",
  year = 2003
}

@Book{BaPOLIS97,
  author = "\mbox{F.~Balarin} et al.",
  title =       "Hardware-software codesign of  embedded systems: The POLIS approach",
  publisher =    "Academic Publishers, Boston",
  year =         1997
}

@book{copelandSoftwareTest03,
  author="Lee Copeland",
  title="A Practitioner's Guide to Software Test Design",
  year="2003",
  publisher="Artech House",
}

@book{parhiVLSI99,
  author = "Keshab K. Parhi",
  title = "VLSI Digital Signal Processing Systems: Design and Implementation",
  publisher = "Wiley-Interscience",
  year = "1999",
  month = "January",
}

@book{endertonLogic2000,
  author = "Herbert B. Enderton",
  title = "A Mathematical Introduction to Logic",
  publisher = "Academic Press",
  year = "2000",
  month = "December",
}

@techreport{norrishC2HOL98,
  author="Michael Norrish",
  title="C Formalized in {HOL}",
  publisher="University of Cambridge Computer Laboratory",
  institution="University of Cambridge Computer Laboratory",
  year="1998",
  month="December",
}

@techreport{BaHetero02,
  author = "F. Balarin and L. Lavagno and C. Passerone and A. Sangiovanni-Vincentelli and M. Sgroi and Y. Watanabe",
  title = "Modeling and designing heterogeneous systems",
  month = "Nov",
  year = "2001",
  publisher = "Cadence Berkeley Laboratories",
  institution = "Cadence Berkeley Laboratories",
}

@book{HOL93,
 editor={M. J. C. Gordon and T. F. Melham},
 title={Introduction to HOL: a theorem proving environment for higher order logic},
 year={1993},
 publisher={Cambridge University Press},
 address={New York, NY, USA},
}

@book{GrotkerSystemC,
  author="T. Grotker and S. Liao and G. Martin and S. Swan",
  title= "System Design with SystemC",
  year  =   "2002",
  publisher =   "Kluwer Academic Publishers",
}

@inproceedings{fujita01standard,
    author = "Masahiro Fujita and Hiroshi Nakamura",
    title = "The standard SpecC language",
    booktitle = "International Symposium on Systems Synthesis",
    year = "2001",
}

@inproceedings{BaMetro03,
  author = "\mbox{F.~Balarin} et al.",
  title = "Metropolis: an integrated electronic system design environment",
  month = "Apr",
  year =      "2003",
  booktitle = "Computer 36",
}

@article{turner-survey,
 author = {J. Turner and N. Yamanaka},
 title = "{Architectural Choices in Large Scale ATM Switches}",
 journal = "{IEICE Transactions}",
  year = 1998,
}

@inproceedings{prakash-infocom-04,
  author = {A. Prakash and A. Aziz and V. Ramachandran},
  title = "{Randomized Parallel Schedulers for Switch-Memory-Switch
	Routers: Analysis and Numerical Studies}",
  booktitle = infocom,
  year = 2004,
}

@InProceedings{MoskewiczETAL01Chaff,
  author =       {Matthew W. Moskewicz and Conor F. Madigan and Ying Zhao and Lintao Zhang and Sharad Malik},
  title =        {Chaff: Engineering an Efficient {SAT} Solver},
  booktitle =    DAC01,
  month =        Jun,
  year =         2001
}

@misc{juniper-sms-patent,
    author = {Juniper Networks},
    title = {High Speed Switching Device},
    year = 1999,
    howpublished = "US Patent 5,905,726"
}

@mastersthesis{FZEdgeFusion2001,
  author = {F. Zaraket},
  title = "{Optimal Fusion and Objective Comparison of Edge Detectors }",
  school = "American University of Beirut",
  year = 2001,
}

@inproceedings{verisoft-icse-02,
  author = {S. Chandra and P. Godefroid and C. Palm},
  title = "{Software model checking in practice: an industrial case study}",
  booktitle = icse,
  year = 2002
}

@inproceedings{BoGu97deadcode,
 author = {Rastislav Bodek and Rajiv Gupta},
 title = {Partial dead code elimination using slicing transformations},
 booktitle = {ACM Conference on Programming language design and implementation},
 year = {1997},
 }

@inproceedings{LiSt99deadcode,
    author = "Yanhong A. Liu and Scott D. Stoller",
    title = "Eliminating Dead Code on Recursive Data",
    booktitle = "Static Analysis Symposium",
    year = "1999",
}


@inproceedings{vis-fmcad-96,
	author = { R. Brayton and G. Hachtel and A. Sangiovanni-Vincentelli and F. Somenzi and A. Aziz and S. Cheng and S. Edwards and S. Khatri and Y. Kukimoto and A. Pardo and S. Qadeer and R.  Ranjan and S. Sarwary  and T. Shiple and G. Swamy and T. Villa},
	title = "{VIS}",
	booktitle = fmcad,
	month = nov,
	year = 1996
}

@inproceedings{BrRoSiConflictSynthesis05,
	author = {Oliver Bringmann and Wolfgang Rosenstiel and Axel Siebenborn},
	title = {Conflict analysis in multiprocess synthesis for optimized system integration},
	booktitle = {International conference on Hardware/software codesign and system synthesis},
	year = {2005},
 }

@inproceedings{seraICSE07,
  author={Fadi Zaraket and Adnan Aziz and Sarfraz Khurshid},
  title={Sequential Circuits for Relational Analysis},
  booktitle={International Conference on Software Engineering},
  year={2007},
  month="May",
}

@inproceedings{sebacASE07,
  author = {Fadi Zaraket and Adnan Aziz and Sarfraz Khurshid},
  title = {Sequential circuits for program analysis},
  booktitle = {IEEE/ACM international conference on Automated software engineering},
  year = {2007},
  location = {Atlanta, Georgia},
  publisher = {ACM},
}


@inproceedings{jpfVisser03visser,
    author = "Willem Visser and Klaus Havelund and Guillaume Brat and Seung-Joon Park",
    title = "Model Checking Programs",
    booktitle = "{A}utomated {S}oftware {E}ngineering Journal",
    year = "2003",
    month = "April",
}

@inproceedings{kodkodTJ2007,
  author="E. Torlak and D. Jackson",
  title="Kodkod: A Relational Model Finder",
  booktitle="Tools and Algorithms for Construction and Analysis of Systems",
  year= "2007",
  month="March",
}

@article{sparkGupta04,
  author = {Sumit Gupta and Rajesh Kumar Gupta and Nikil D. Dutt and Alexandru Nicolau},
  title = {Coordinated parallelizing compiler optimizations and high-level synthesis},
  journal = {ACM Transactions on Design Automation of Electronic Systems},
  year = {2004},
  month="October",
}

@phdthesis{schedulingHaynal00,
  author={S. Haynal},
  title={Automata-Based Symbolic Scheduling},
  year="2000",
  school="University of California, Santa Barbara",
}

@inproceedings{cbmcCKL2004,
  AUTHOR    = { Edmund Clarke and Daniel Kroening and Flavio Lerda},
  TITLE     = { A Tool for Checking {ANSI-C} Programs },
  BOOKTITLE = { Tools and Algorithms for the Construction and Analysis of Systems},
  YEAR      = { 2004 },
  MONTH     = "March",
}


@inbook{findTheBugBarr02,
  author =  "Adam Barr",
  year  =   "2002",
  publisher =   "Addison-Wesley",
  title =   "Find The Bug: A Book of Incorrect Programs"
}

@PHDTHESIS{Kuncak07Thesis,
  author = {Viktor Kuncak},
  title = {Modular Data Structure Verification},
  school = {EECS Department, Massachusetts Institute of Technology},
  month = {February},
  year = {2007}
}

@inproceedings{FuMalik2007,
    author = {Zhaohui Fu and Sharad Malik},
    title = {Extracting Logic Circuit Structure from
              Conjunctive Normal Form Descriptions},
    booktitle = {Proceedings of International Conference on VLSI
              Design},
    month = {January},
    year = {2007},
}

@article{Momtahan05,
  author    = {Lee Momtahan},
  title     = {Towards a Small Model Theorem for Data Independent Systems
               in Alloy.},
  journal   = {Electronic Notes in Theoretical Computer Science},
  year      = {2005},
}
%  pages     = {37-52},
%  volume    = {128},
%  number    = {6},
%  ee        = {http://dx.doi.org/10.1016/j.entcs.2005.04.003},
%  bibsource = {DBLP, http://dblp.uni-trier.de}
%}

@inproceedings{clarke04Predicate,
  author = "E. Clarke and D. Kroening and N. Sharygina and K. Yorav",
  title = "Predicate Abstraction of ANSI-C Programs using SAT",
  booktitle = "Formal Methods in System Design",
  year = "2004",
}

@inproceedings{janic97PAcompare,
  author = {P. Janicic and I. Green and A. Bundy},
  title = "A comparison of decision procedures in Presburger arithmetic",
  booktitle = {LIRA: Logic and Computer Science},
  year = "1997",
}
%  text = "P. Janicic, I. Green, and A. Bundy. A comparison of decision procedures
%    in Presburger arithmetic, October 1997. Research paper #872, Division of
%    Informatics, University of Edinburgh.",

@InBook{McMillan03,
	title = { Interpolation and SAT-Based Model Checking},
	author = {K. L. McMillan},
	booktitle= {Computer Aided Verification},
	year = 2003,
	publisher = {Springer Berlin / Heidelberg}
}

@article{bryant86,
    author = {R. Bryant},
    title = "{Graph-based Algorithms for Boolean Function Manipulation}",
    journal = ieeetc,
    volume = {C-35},
    pages = {677-691},
    month = aug,
    year = 1986
}

@article{ edwards97design,
    author = "S.~Edwards and L.~Lavagno and E. A.~Lee and A.~Sangiovanni-Vincentelli",
    title = "Design of Embedded Systems: Formal Models, Validation, and Synthesis",
    journal = "Proc. of the IEEE",
    volume = "85",
    year = "1997",
}

@article{Roop02k-timeSim,
  author = {Partha S. Roop and A. Sowmya and S. Ramesh},
  title = {k-time Forced Simulation: A Formal Verification Technique for IP Reuse},
  journal = {International Conference on Computer Design},
  year = {2002},
  publisher = {IEEE Computer Society},
}

@InBook{jackson:abstraction,
  author = 	 {Daniel Jackson and Michael Jackson},
  title = 	 {Software Abstractions: Logic, Language, and Analysis},
  publisher = MIT-P,
  year=2006,
}

%  editor = 	 {M. Butler and C. Jones and A. Romanovsky and E. Troubitsyna},
%  chapter = 	 {Rigorous development of complex fault tolerant systems},
@techreport{brayton92sis,
        author = {E. M. Sentovich and K. J. Singh and L. Lavagno and C. Moon
                  and R. Murgai and A. Saldanha and H. Savoj and P. R.
                  Stephan and R. K. Brayton and A. L. Sangiovanni-Vincentelli},
        title = "{SIS: A System for Sequential Circuit Synthesis}",
        address = {Univ. of California, Berkeley},
        month = may,
        year = 1992,
        institution = erl,
}

@techreport{EdLeePtolemy03,
  author = "Edward A. Lee",
  title = "Overview of the Ptolemy Project",
  month = "Jul",
  year = "2003",
  publisher = "Cadence Berkeley Laboratories",
  institution = "University of California, Berkeley",
}

@inproceedings{fujita01standard,
    author = "Masahiro Fujita and Hiroshi Nakamura",
    title = "The standard SpecC language",
    booktitle = "International Symposium on Systems Synthesis",
    year = "2001",
}

@Book{BaPOLIS97,
  author = "\mbox{F.~Balarin} et al.",
  title =       "Hardware-software codesign of  embedded systems: The POLIS approach",
  publisher =    "Academic Publishers, Boston",
  year =         1997,
}

@inproceedings{CVCLite,
  author="Clark Barrett and Sergey Berezin",
  title="CVC Lite: A new implementation of the cooperating validity checker",
  booktitle="Computer Aided Verification", 
  month = "April",
  year = "2004",
}

@inproceedings{BaMetro03,
  author = "\mbox{F.~Balarin} et al.",
  title = "Metropolis: an integrated electronic system design environment",
  month = "Apr",
  year =      "2003",
  booktitle = "Computer 36",
}

@inproceedings{Hildreth80EdgeDetection,
  author = "D. Marr and E. Hildreth",
  title = "Theory of Edge Detection",
  year = "1980",
  booktitle = "the Royal Society of London",
}

@inproceedings{HolzSpin97,
  author="G. Holzmann",
  title="The model checker {SPIN}",
  booktitle="IEEE Transactions on Software Engineering",
  month="May",
  year="1997",
}


@techreport{BaHetero02,
  author = "F. Balarin and L. Lavagno and C. Passerone and A. Sangiovanni-Vincentelli and M. Sgroi and Y. Watanabe",
  title = "Modeling and designing heterogeneous systems",
  month = "Nov",
  year = "2001",
  publisher = "Cadence Berkeley Laboratories",
  institution = "Cadence Berkeley Laboratories",
}

@inproceedings{Fei06coverify,
  author = "Fei Xie and Guowu Yang and Xiaoyu Song",
  title = "Component-based hardware/software co-verification",
  year = "2006",
  month = "July",
  booktitle = "Formal Methods and Models for Co-Design"
}

@inproceedings{gerth96LTL,
  author = {Rob Gerth and Doron Peled and Moshe Y. Vardi and Pierre Wolper},
  title = {Simple on-the-fly automatic verification of linear temporal logic},
  booktitle = {International Symposium on Protocol Specification, Testing and Verification},
  year = {1996},
}

@book{GrotkerSystemC,
  author="T. Grotker and S. Liao and G. Martin and S. Swan",
  title= "System Design with SystemC",
  year  =   "2002",
  publisher =   "Kluwer Academic Publishers",
}
  

@InProceedings{KhJuzi03,
  author = "S. Khurshid and C. Pasareanu and W. Visser",
  title = "Generalized symbolic execution for model checking and testing",
  booktitle = "International Conference on Tools and Algorithms for the Construction and Analysis of Systems",
  year = "2003",
  month = "Apr",
}

@article{KingSE76,
 author = {James C. King},
 title = {Symbolic execution and program testing},
 journal = {Communications of the ACM},
 volume = {19},
 number = {7},
 year = {1976},
 publisher = {ACM Press},
 }


@inproceedings{chiodo95synthesis,
    author = "Massimiliano Chiodo and Paolo Guisto and Attila Jurecska and Luciano Lavagno and Harry Hsieh and Kei Suzuki and Alberto L. Sangiovanni-Vincentelli and Ellen Sentovich",
    title = "Synthesis of Software Programs for Embedded Control Applications",
    booktitle = "Design Automation Conference",
    year = "1995",
}

@inproceedings{ chiodo93synthesis,
    author = "{M. Chiodo} and {P. Giusto} and {H. Hsieh} and {A. Jurecska} and {L. Lavango} and {A. Sangiovanni-Vincentelli}",
    title = "Synthesis of Mixed Software-Hardware Implementation from {CFSM} Specifications",
    booktitle = "International Workshop on Hardware-Software Codesign",
    year = "1993",
}


@article{ACL2Kaufmann97,
    author = "Matt Kaufmann and J. Strother Moore",
    title = "An Industrial Strength Theorem Prover for a Logic Based on Common Lisp",
    journal = "Software Engineering",
    volume = "23",
    number = "4",
    pages = "203--213",
    year = "1997",
}

@InProceedings{monaCav98,
  author = 	 {Jacob Elgaard and Nils Klarlund and Anders M�ller},
  title = 	 {Mona 1.x: new techniques for WS1S and WS2S},
  booktitle = 	 cav,
  year =	 1998,
  publisher =	 {Springer Verlag}
}

@MastersThesis{dennis03:_tsafe,
  author = 	 {Greg Dennis},
  title = 	 {{TSAFE}: Building a Trusted Computing Base for Air Traffic Control Software},
  school = 	 {Massachusetts Institute of Technology},
  year = 	 2003
}

@InProceedings{lahiri04uclid,
  author = "S. Lahiri and S. Seshia",
  title = "The UCLID decision procedure",
  booktitle = cav,
  year = "2004",
}

@InProceedings{Adjie-WinotoETAL99IntentionalNamingSystem,
  Author =       {William Adjie-Winoto and Elliot Schwartz and Hari Balakrishnan and Jeremy Lilley},
  Title =        {The Design and Implementation of an Intentional Naming System},
  Booktitle =    SOSP99,
  Address =      {Kiawah Island},
  Month =        Dec,
  Year =         1999
}

@Book{Box98EssentialCOM,
  author = {D. Box},
  title = {Essential {COM}},
  publisher = {Addison Wesley},
  year = 1998
}


@InProceedings{de-micheli1999hardware,
author =       {Giovanni {De Micheli}},
title =        {Hardware Synthesis from {C/C++} Models},
booktitle =    date, 
year =         1999,
month =        mar
}
%pages =        {382--383},
%address =      {Munich, Germany},

@InProceedings{edwards2005challenges,
author =       {Stephen A. Edwards},
title =        {The Challenges of Hardware Synthesis from {C}-like 
                Languages},
booktitle =    date,
year =         2005
}
%month =        mar
%pages =        {66--67},
%address =      {Munich, Germany},


@Book{CormenETAL90IntroductionAlgorithms,
  author =       {Thomas H. Cormen and Charles E. Leiserson and Ronald L. Rivest},
  title =        {Introduction to Algorithms},
  publisher =    MIT-P,
  year =         1990
}

@Manual{Jackson04Alloy3,
  author =       {Daniel Jackson},
  title =        {Alloy 3.0 Reference Manual},
  month =        May,
  year =         2004,
  note =         {http://alloy.mit.edu/reference-manual.pdf}
}
%  note =         {\texttt{http://alloy.mit.edu/reference-manual.pdf}}

@InProceedings{ andoni-evaluating,
  author = "A. Andoni and D. Daniliuc and S. Khurshid and D. Marinov",
  title = "Evaluating the small scope hypothesis",
  text = "Alexandr Andoni, Dumitru Daniliuc, Sarfraz Khurshid, and Darko Marinov.
    Evaluating the small scope hypothesis. submitted for publication.",
  url = "citeseer.ist.psu.edu/623993.html" }

@InProceedings{Hari05expert,
  author = "\mbox{H.~Mony} et al.",
  title = "Scalable Automated Verification via Expert-System Guided Transformations",
  booktitle = "Formal Methods in Computer-Aided Design",
  month = Nov,
  year = "04",
}

@InProceedings{ boyapati02korat,
  author = "C. Boyapati and S. Khurshid and D. Marinov",
  title = "Korat: Automated testing based on Java predicates",
  booktitle = "International Symposium on Software Testing and Analysis, Rome, Italy",
  month = July,
  year = "2002",
 }

@InProceedings{ Zara05,
  author = "F. Zaraket and J. Baumgartner and A. Aziz",
  title = "Scalable Compositional Minimization via Static Analysis",
  booktitle = "International Conference on Computer Aided Design",
  month = Nov,
  year = "2005",
 }

@inproceedings{Aloul02SymSAT,
 author = {Fadi A. Aloul and Arathi Ramani and Igor L. Markov and Karem A. Sakallah},
 title = {Solving difficult SAT instances in the presence of symmetry},
 booktitle = {Design automation conference},
 year = {2002},
 isbn = {1-58113-461-4},
 location = {New Orleans, Louisiana, USA},
 doi = {http://doi.acm.org/10.1145/513918.514102},
 publisher = {ACM Press}
}
% address = {NY, USA},
%  pages = {731--736},

@InProceedings{FULLBayardo97UsingCSPSAT,
  author =       {Roberto J. {Bayardo Jr.} and Robert C. Schrag},
  title =        {Using {CSP} look-back techniques to solve real world {SAT} instances},
  booktitle =    NAI97,
  year =         1997
}
%  pages =        {203--208},

@book{kurshan93,
        author = {R. P. Kurshan},
        title = "{Automata-Theoretic Verification of Coordinating Processes}",
        publisher = {Princeton University Press},
        year = 1993
}

@techreport{brayton92sis,
        author = {E. M. Sentovich and K. J. Singh and L. Lavagno and C. Moon
                  and R. Murgai and A. Saldanha and H. Savoj and P. R.
                  Stephan and R. K. Brayton and A. L. Sangiovanni-Vincentelli},
        title = "{SIS: A System for Sequential Circuit Synthesis}",
        address = {Univ. of California, Berkeley},
        month = "May",
        year = 1992,
        institution = erl,
}




@inproceedings{GraMcco92,
 author = {E. Gradel and G.L. McColm},
 title = {Deterministic vs. nondeterministic transitive closure logic},
 booktitle = {LiCS:  Logic in Computer Science. Proceedings of the 7th IEEE Symposium},
 year = {1992}
}
% pages = {58--63},

@article{Floyd82RegExp,
 author = {Robert W. Floyd and Jeffrey D. Ullman},
 title = {The Compilation of Regular Expressions into Integrated Circuits},
 journal = {J. ACM},
 volume = {29},
 number = {3},
 year = {1982},
 issn = {0004-5411},
 doi = {http://doi.acm.org/10.1145/322326.322327},
 publisher = {ACM Press}
}
% pages = {603--622},
% address = {New York, NY, USA},

@inproceedings{SeaBre93,
 author = {Andrew Seawright and Forrest Brewer},
 title = {High-level symbolic construction technique for high performance sequential synthesis},
 booktitle = DAC,
 year = {1993},
}
% pages = {424--428},
% address = {New York, NY, USA},

@inproceedings{OliHu02,
 author = {Marcio T. Oliveira and Alan J. Hu},
 title = {High-Level specification and automatic generation of {IP} interface monitors},
 booktitle = {Design Automation Conference},
 year = {2002},
}
% address = {New York, NY, USA},
% booktitle = {DAC '02: Proceedings of the 39th conference on Design automation},

@inproceedings{Jackson00,
 author = {Daniel Jackson},
 title = {Automating first-order relational logic},
 booktitle = {ACM-SIGSOFT Symposium on Foundations of Software Engineering},
 year = {2000},
}
% address = {New York, NY, USA},
% pages = {130--139},

@phdthesis{Shlya05,
  author =  "Ilya A Shlyakhter",
  year  =   "2005",
  month =   "February",
  school =  "MIT",
  title =   "Declarative Symbolic Pure-Logic Model Checking"
}

@inproceedings{Jackson98,
 author = {Daniel Jackson},
 title = {An intermediate design language and its analysis},
 booktitle = {ACM-SIGSOFT Symposium on Foundations of Software Engineering},
 year = {1998},
}
%  pages = {121--130},
% address = {New York, NY, USA},
% booktitle = {ACM-SIGSOFT '98/FSE-6: Proceedings of the 6th ACM SIGSOFT international symposium on Foundations of software engineering},

@article{BuClMcDiHw92,
 author = {J. R. Burch and E. M. Clarke and K. L. McMillan and D. L. Dill and L. J. Hwang},
 title = {Symbolic model checking: $10^{20}$ states and beyond},
 journal = {Information and Computation},
 volume = {98},
 number = {2},
 year = {1992},
}
% address = {Duluth, MN, USA},
% pages = {142--170},


@inproceedings{HmBPK05,
  author = "Hari Mony and Jason Baumgartner and Viresh Paruthi and Robert Kanzelman",
  title =     "Exploiting Suspected Redundancy without Proving It",
  year =      "2005",
  booktitle = "Design Automation Conference",
  publisher = {ACM Press}
}
%  month = "June",

@inproceedings{PDChBoy,
  author = "P. Darga and C. Boyopati",
  title =     "Language and analysis techniques for efficient software model checking",
  month = "Jan",
  year =      "2006",
  booktitle = "POPL",
}


@inproceedings{RWCleave,
  author = "R. W. Cleaveland and J. Parrow and B. Steffen",
  title =     "The concurrency oworkbench",
  year =      "1989",
  booktitle = "International workshop on Automatic verification methods for finite state systems",
}

@inproceedings{PGode,
  author = "P. Godefroid",
  title =     "Using partial orders to improve automatic verification methods",
  year =      "1990",
  booktitle = "2nd Workshop on Computer-Aided Verification",
}


@inproceedings{DanJack,
  author = "Daniel Jackson",
  title =     "Abstract model checking of inifinite specifications",
  month = "Oct",
  year =      "1994",
  booktitle = "Formal Methods, {E}urope, {B}arcelona",
}

@inproceedings{KhdMar,
  author = "Sarfraz Khurshid and Darko Marinov",
  title =     "TestEra: Specification-based Testing of Java Programs Using SAT",
  month = "Oct",
  year =      "2004",
  booktitle = "Automated Software Engineering Journal",
}

@inproceedings{BoyKhd,
  author = " C. Boyapati, S. Khurshid and D. Marinov",
  title =     "Korat: Automated Testing Based on Java Predicates",
  month = "Jul",
  year =      "2002",
  booktitle = "International Symposium on Software Testing and Analysis",
}

@inproceedings{KhdPaVi,
  author = " S. Khurshid, C. Pasareanu and W. Visser",
  title =     "Generalized Symbolic Execution for Model Checking and Testing",
  month = "Apr",
  year =      "2003",
  booktitle = "International Conference on Tools and Algorithms for Construction and Analysis of Systems",
}


@inproceedings{BaMo05,
  author =       "Jason Baumgartner and Hari Mony",
  title =        "Maximal Input Reduction of Sequential Netlists Via
                 Synergistic Reparameterization and Localization
                 Strategies",
  year      =    "2005",
  month     =    "Oct.",
  booktitle =    "Correct Hardware Design and Verification Methods",
}

@inproceedings{JuKeAdCa,
  author =  "Jun Yuan and Ken Albin and Adnan Aziz and Carl Pixley",
  booktitle =   "Proceedings of the Design Automation Conference",
  year  =   "2003",
  month =   "June",
  pages =   "296-299",
  title =   "Constraint Synthesis for Environment Modeling in Functional Verification"
}

@book{Kropf98,
  author="Thomas Kropf",
  year="1998",
  title="Introduction to Formal Hardware Verification",
  publisher="Springer-Verlag",
}

@book{EdOrPe,
  author="Edmund Clarke and Jr. Orna Brumberg and Doron A. Peled",
  year="1999",
  publisher ="MIT Press",
  title="Model Checking"
}
  %pages =       "194-203",
  %chapter =     "13",

@incollection{KuE01,
  author =  "Andreas Kuehlmann and Cornelis A.J. van Eijk",
  year  =   "2001",
  editor =  "S. Hassoun and T. Sasao",
  chapter =     "13",
  pages  =      "343--369",
  publisher =   "Kluwer Academic Publisher",
  title =   "Combinational and Sequential Equivalence Checking",
  booktitle =   "Logic Synthesis and Verification"
}

@inproceedings{ViYoBr,
  author =  "Vigyan Singhal and Yosinori Watanabe and Robert Brayton",
  booktitle =   "International Conference on Computer Design",
  address =     "Department of Electrical Engineering and Computer Sciences, University of California, Berkley, CA",
  title =       "Heuristic Minimization for Synchronous Relations",
  pages =       "428-433",
  year =        "1993"

}

@inproceedings{NeBiCP,
  author =  "Bill Lin and  A. Richard Newton",
  booktitle =   "International Conference on Computer Design",
  year    =     "1991",
  month =       "Oct",
  title =       "Implicit Manipulation of Equivalence Classes Using Binary decision Diagrams"
}

@inproceedings{JuYuCa,
  author =  "Jun Yuan and Kurt Shultz and Carl Pixley and Hillel Miller and Adnan Aziz",
  booktitle =   "IEEE Design Automation Conference",
  year    =     "1999",
  month =       "NA",
  pages =       "NA",
  title =       "Modeling Design Constraints and Biasing in Simulation Using BDDs"
}


@inproceedings{NeBiLin,
  author =  "Bill Lin and Herve J. Touati and A. Richard Newton",
  booktitle =   "Design Automation Conference",
  year    =     "1990",
  month =       "June",
  title =       "Don't Care Minimization of Multi-Level Sequential Logic Networks"
}

@inproceedings{MauMic,
  author =  "Maurizio Damiani and Giovanni De Micheli",
  booktitle =   "IEEE Design Automation Conference",
  year    =     "1992",
  month =       "June",
  pages =       "556--561",
  title =       "Recurrence Equations and the Optimization of Synchronous Logic Circuits"
}

@incollection{CILDoc,
  author =  "George Necula et al.",
  booktitle =   "Documentation",
  publisher =   "Berkeley University",
  address =     "http://www.eecs.berkeley.edu/~necula/cil/",
  title =       "CIL - Infrastructure for C Program Analysis and Transformation",
}

@incollection{JvAss,
  author =  "Shigeru Chiba and Muga Nishizawa",
  booktitle =   "Int'l Conf. on Generative Programming and Component Engineering",
  publisher = "Springer-Verlag",
  year=  "2003",
  address =     "http://www.csg.is.titech.ac.jp/~chiba/javassist",
  title =       "An Easy-to-Use Toolkit for Efficient Java Bytecode Translators ",
}

@incollection{WegGol,
  author =  "Peter Wegner and Dina Goldin",
  booktitle =   "Technical Report",
  publisher =   "Brown University",
  address =     "http://www.cs.brown.edu/people/pw/home.html",
  year   =      "1999",
  month =       "January",
  title =       "Mathematical Models of Intercative Computing"
}

@Article{GiStPa,
  author =  "Gianpiero Cabodi and Stefano Quer and Paolo Camurati",
  year  =   "1995",
  journal = "IEEE Transactions on Computer-Aided Design",
  number =      "1063-6404",
  title =   "Extending Equivalence Class Computation to Large {FSM}s",
  pages =   "258--263"
}

@article{aziz00S1S,
  author = "Adnan Aziz and Felice Balarin and R Brayton and A Sangiovanni-Vincentelli",
  title = "Sequential Synthesis Using {S1S}",
  journal = "IEEE Transactions on Computer-Aided Design of Integrated Circuits",
  year = "2000",
}
%  volume = "19",

@inproceedings{Syn02a,
  author =  "In-Ho Moon and Hee Hwan Kwak and James Kukula and Thomas Shiple and Carl Pixley",
  booktitle =   "Formal Methods in Computer-Aided Design",
  year  =   "2002",
  month =   "Nov.",
  title =   "Simplifying Circuits for Formal Verification Using Parametric Representation"
}
 %  pages =   "52--69",

@inproceedings{ShRaBrBr,
  author =  "Shuvendu K. Lahiri and E. Randal and E. Bryant and Bryon Cook",
  booktitle =   "Computer-Aided Verification",
  month =       "July",
  year  =   "2003",
  pages =   "141-153",
  title =   "A Symbolic Approach to Predicate Abstraction"
}

@inproceedings{EdOrMuDo,
  author =  "Edmund Clarke and Orna Grumberg and Muralidhar Talupur and Dong Wang",
  booktitle =   "Computer-Aided Verification",
  month =       "July",
  year  =   "2003",
  pages =   "126-140",
  title =   "Making Predicate Abstraction Efficient"
}

@inproceedings{ShKuRan98,
  author =  "Thomas Shiple and James Kukula and Rajeev Ranjan",
  booktitle =   "Computer-Aided Verification",
  year  =   "1998",
  month =   "June",
  title =   "A Comparison of Presburg Engines for EFSM Reachability"
}

@inproceedings{AdJiTo,
  author =  "Adnan Aziz and Jim Kukula and Tom Shiple",
  booktitle =   "Proceedings of the 35th Design Automation Conference",
  year  =   "1998",
  month =   "June",
  title =   "Hybrid Verification Using Saturated Simulation"
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%Neil Weste and Kamran Eshraghian. Principles of CMOS VLSI Design - A System Perspective. Second Edition, Addison-Wesley Publishing Co. 1993, pp.208 - 226.
@book{weste_book,
  author =  "N. Weste and D. Harris",
  year  =   "2005",
  publisher =   "Addison-Wesley Publishing Company",
  title =   "CMOS VLSI Design - A Circuits and Systems Perspective."
}

@book{vhdl,
	author= "P. Ashenden",
	year = 2002,
	title = "The Designers Guide to VHDL",
	publisher = "Morgan Kaufmann",
}

@book{WeEs93,
  author =  "Neil Weste and Kamran Eshraghian",
  year  =   "1993",
  publisher =   "Addison-Wesley Publishing Company",
  title =   "Principles of CMOS VLSI Design - A System Perspective. Second Edition"
}

@Article{KuPKG02,
  author =  "Andreas Kuehlmann and Viresh Paruthi and Florian Krohm and Malay Ganai",
  year  =   "2002",
  journal = "IEEE Transactions on Computer-Aided Design",
  title =   "Robust {B}oolean Reasoning for Equivalence Checking and Functional Property Verification",
  volume =  "21",
  number =  "12"
}
%  pages =   "1377--1384",
%  month =  "Dec.",



@book{Fo00,
  author =  "John J. Forrest",
  publisher =        "Personal communication",
  year =        "2000"
}

@inproceedings{Wolf91a,
  author =  "Wolf, W.",
  booktitle =   "European Conference on Design Automation",
  year  =   "1991",
  month =   "February",
  publisher =   "IEEE",
  pages =   "378--382",
  title =   "Decomposing Data Machines"
}

@inproceedings{KuD92,
  author =  "Kung, D. S. and Damiano, R. F. and Nix, T. A. and Geiger, D. J.",
  booktitle =   "Proceedings of the 29th Design Automation Conference",
  year  =   "1992",
  month =   "June",
  pages =   "484--487",
  title =   "{BDDMAP}: a technology mapper based on a new covering algorithm"
}

@incollection{BaLM87,
  author =  "Baitinger, U. G. and Lipp, H. M. and Mlynski, D. A. and Reiss, K.",
  booktitle =   "Design Systems for {VLSI} Circuits",
  year  =   "1987",
  editor =  "G. {De Micheli} and A. {Sangiovanni-Vincentelli} and P. Antognetti",
  publisher =   "Martinus Nijhoff Publishers",
  pages =   "527--537",
  series =  "Applied Sciences - No. 136",
  title =   "The {MEGA} System for Semi-Custom Design"
}

@incollection{DeRS87,
  author =  "H. {De Man} and J. Rabaey and P. Six",
  booktitle =   "Design Systems for {VLSI} Circuits",
  year  =   "1987",
  editor =  "G. {De Micheli} and A. {Sangiovanni-Vincentelli} and P. Antognetti",
  publisher =   "Martinus Nijhoff Publishers",
  pages =   "571--645",
  series =  "Applied Sciences - No. 136",
  title =   "{CATHEDRAL II}: A Synthesis and Module Generation System for Multiprocessor Systems on a Chip"
}

@incollection{WaTL91,
  author =  "W. Wolf and A. Takach and T.-C. Lee",
  booktitle =   "High-Level {VLSI} Synthesis",
  year  =   "1991",
  editor =  "R. Camposano and W. Wolf",
  publisher =   "Kluwer Academic Publishers",
  pages =   "231--254",
  title =   "Architectural Optimization Methods for Control-Dominated Machines"
}

@inproceedings{BjesseC00,
    author = "Per Bjesse and Koen Claessen",
    title = "{SAT}-Based Verification without State Space Traversal",
    booktitle = "Formal Methods in Computer-Aided Design",
    month = "November",
    year = "2000"
}
%    pages = "372--389",


@inproceedings{KiFN91,
  author =  "James J. Kim and Fadi J. Kurdahi and Nohbyung Park",
  booktitle =   "Int'l Conference on Computer-Aided Design",
  year  =   "1991",
  month =   "Nov.",
  pages =   "30--33",
  title =   "Automatic Synthesis of Time-Stationary Controllers for Pipelined Data Paths"
}

@inproceedings{AlVG91,
  author =  "Allen C-H Wu and Viraphol Chaiyakul and Daniel D. Gajski",
  booktitle =   "Int'l Conference on Computer-Aided Design",
  year  =   "1991",
  month =   "Nov.",
  pages =   "34--37",
  title =   "Layout-Area Models for High-Level Synthesis"
}

@inproceedings{LiHH91,
  author =  "Shi-Zheng Lin and Cheng-Tsung Hwang and Yu-Chin Hsu",
  booktitle =   "Int'l Conference on Computer-Aided Design",
  year  =   "1991",
  month =   "Nov.",
  pages =   "38--41",
  title =   "Efficient Microcode Arrangement and Controller Synthesis"
}

@inproceedings{Berg91,
  author =  "Reinaldo A. Bergamaschi",
  booktitle =   "Int'l Conference on Computer-Aided Design",
  year  =   "1991",
  month =   "Nov.",
  pages =   "80--83",
  title =   "The Effects of False Paths in High-Level Synthesis"
}

@inproceedings{KiLL91,
  author =  "Taewhan Kim and Jane W. S. Liu and C. L. Liu",
  booktitle =   "Int'l Conference on Computer-Aided Design",
  year  =   "1991",
  month =   "Nov.",
  pages =   "84--87",
  title =   "A Scheduling Algorithm For Conditional Resource Sharing"
}

@inproceedings{PoR91,
  author =  "Miodrag Potkonjak and Jan Rabaey",
  booktitle =   "Int'l Conference on Computer-Aided Design",
  year  =   "1991",
  month =   "Nov.",
  pages =   "88--91",
  title =   "Optimizing Resource Utilization using Transformations"
}

@inproceedings{LoG91,
  author =  "Loganath Ramachandran and Daniel D. Gajski",
  booktitle =   "Int'l Conference on Computer-Aided Design",
  year  =   "1991",
  month =   "Nov.",
  pages =   "92--95",
  title =   "An Algorithm for Component Selection in Performance Optimized Scheduling"
}

@inproceedings{CoS91,
  author =  "Amnon Baron Cohen and Michael Shechory",
  booktitle =   "Int'l Conference on Computer-Aided Design",
  year  =   "1991",
  month =   "Nov.",
  pages =   "102--105",
  title =   "Track Assignment in the Pathway Datapath Layout Assembler"
}

@inproceedings{ArES91,
  author =  "H. M. A. M. Arts and J. T. J. Eijndhoven and L. Stok",
  booktitle =   "Int'l Conference on Computer-Aided Design",
  year  =   "1991",
  month =   "Nov.",
  pages =   "106--109",
  title =   "Flexible Block-Multiplier Generation"
}

@inproceedings{key0,
  author =  "Srinivas Devadas and Kurt Keutzer and Sharad Malik",
  booktitle =   "Int'l Conference on Computer-Aided Design",
  year  =   "1991",
  month =   "Nov.",
  pages =   "176--179",
  title =   "Delay Computation in Combinatorial Logic Circuits"
}

@inproceedings{McSS91,
  author =  "Patrick C. {McGeer} and Alexander Saldanha and Paul R. Stephan and Robert K. Brayton and Alberto L. {Sangiovanni-Vincentelli}",
  booktitle =   "Int'l Conference on Computer-Aided Design",
  year  =   "1991",
  month =   "Nov.",
  pages =   "180--183",
  title =   "Timing Analysis and Delay-Fault Test Generation using Path-Recursive Functions"
}

@inproceedings{SiSV91,
  author =  "Jo\~{a}o P. Silva and Karem A. Sakallah and Lu\'{\is} M. Vidigal",
  booktitle =   "Int'l Conference on Computer-Aided Design",
  year  =   "1991",
  month =   "Nov.",
  pages =   "212--215",
  title =   "{FDP} - An Environment for Exact Timing Analysis"
}

@inproceedings{MuH91,
  author =  "Andreas M{\"}unzner and G{\"}unter Hemme",
  booktitle =   "Int'l Conference on Computer-Aided Design",
  year  =   "1991",
  month =   "Nov.",
  pages =   "368--371",
  title =   "Converting Combinatorial Circuits into Pipelined Data Paths"
}

@article{SpTh91,
  author =  "David Springer and D. E. Thomas",
  year  =   "1991",
  month =   "Dec.",
  publisher =   "Elsevier Science Publishers B.V.",
  journal = "INTEGRATION, the VLSI journal",
  number =  "6",
  pages =   "267--292",
  title =   "New methods for coloring and clique partitioning in data path allocation",
  volume =  "12"
}

@article{John85,
  author =  "David S. Johnson",
  year  =   "1985",
  publisher =   "Academic Press, Inc.",
  journal = "Journal of Algorithms",
  number =  "6",
  pages =   "434--451",
  title =   "The {NP}-Completeness Column: an Ongoing Guide"
}

@article{GaJo80,
  author =  "M. R. Garey and D. S. Johnson and G. L. Miller and C. H. Papadimitriou",
  year  =   "1980",
  month =   "June",
  publisher =   "Society for Industrial and Applied Mathematics",
  journal = "SIAM Journal Algebraic and Discrete Methods",
  number =  "2",
  pages =   "216--227",
  title =   "The Complexity of Coloring Circular Arcs and Chords",
  volume =  "1"
}

@book{Zah91,
  author =  "Rumi Zahir",
  year  =   "1991",
  editor =  "Wolfgang Fichtner and Walter Guggenb{\"}uhl and Hans Melchior and Geoerge S. Moschytz",
  publisher =   "Hartung-Gorre Verlag",
  key =     "HLS, TCON",
  series =  "Series in microelectronics",
  title =   "Controller Synthesis for Application Specific Integrated Circuits",
  volume =  "16"
}

@inproceedings{Zah89,
  author =  "Rumi Zahir and Wolfgang Fichtner",
  booktitle =   "Fourth Int'l Workshop on High-Level Synthesis",
  year  =   "1989",
  month =   "Oct.",
  publisher =   "ACM",
  title =   "Making Use of Timing Constaints for Controller Synthesis"
}

@inproceedings{ZaFi90,
  author =  "Rumi Zahir and Wolfgang Fichtner",
  booktitle =   "Int'l Workshop on Timing Issues in the Specification and Synthesis of Digital Systems",
  year  =   "1990",
  month =   "August",
  publisher =   "ACM/IEEE",
  title =   "Specification of Timing Constaints for Controller Synthesis"
}

@inproceedings{ZaFi91,
  author =  "Rumir Zahir and Wolfgang Fichtner",
  booktitle =   "Proceedings of The European Conference on Design Automation",
  year  =   "1991",
  month =   "February",
  publisher =   "IEEE",
  key =     "HLS, TCON",
  pages =   "316--322",
  title =   "Specification of Timing Constaints for Controller Synthesis"
}

@inproceedings{Bor88,
  author =  "Gaetano Borriello",
  booktitle =   "Int'l Conference on Computer-Aided Design",
  year  =   "1988",
  month =   "Nov.",
  key =     "INT_FACE, HLS, TCON",
  pages =   "56--59",
  title =   "Combining Event and Data-Flow Graphs in Behavioral Synthesis"
}

@article{HiSC82,
  author =  "Robert B. Hitchcock and Gordon L. Smith and David D. Cheng",
  year  =   "1982",
  month =   "Jan.",
  journal = "IBM Journal of Research and Development",
  number =  "1",
  pages =   "100--105",
  title =   "Timing Analysis of Computer Hardware",
  volume =  "26"
}

@inproceedings{Hit82,
  author =  "Robert B. Hitchcock",
  booktitle =   "Nineteenth Design Automation Conference Proceedings",
  year  =   "1982",
  month =   "June",
  title =   "Timing Verification and the Timing Analysis Program"
}

@inproceedings{BrI86,
  author =  "Daniel Brand and Vijay S. Iyengar",
  booktitle =   "Int'l Conference on Computer-Aided Design",
  year  =   "1986",
  month =   "Nov.",
  pages =   "126--129",
  title =   "Timing Analysis using Functional Relationships"
}

@techreport{BrI86b,
  author =  "Daniel Brand and Vijay S. Iyengar",
  year  =   "1986",
  month =   "March",
  number =  "Computer Science, RC 11768 (\#52821)",
  pages =   "25",
  institution = "IBM Research Division, T. J. Watson Research Center, Yorktown Heights, NY 10598",
  title =   "Timing Analysis using Functional Relationships"
}

@techreport{McCune94,
  author =  "William McCue",
  year  =   "1994",
  month =   "May",
  institution = "Argonne National Laboratory",
  title =   "A Davis-Putnam Program and its Application to Finite First-Order Model Search: Quasigroup Existence Problems",
  html =    "http://blankenburg.watson.ibm.com:8001/html/dac94/dac94.html"
}

@article{BrI88,
  author =  "Daniel Brand and Vijay S. Iyengar",
  year  =   "1988",
  month =   "Oct.",
  journal = "IEEE Transactions on Computers",
  number =  "10",
  pages =   "1309--1314",
  title =   "Timing Analysis using Functional Analysis",
  volume =  "37"
}

@article{KirC66,
  author =  "T. I. Kirkpatrick and N. R. Clark",
  year  =   "1966",
  month =   "March",
  journal = "IBM Journal of Research and Development",
  number =  "2",
  pages =   "135--141",
  title =   "{PERT} as an Aid to Logic Design",
  volume =  "10"
}

@inproceedings{WaS86,
  author =  "David E. Wallace and Carlo H. S\'e quin",
  booktitle =   "Proceedings of the 23rd Design Automation Conference",
  year  =   "1986",
  month =   "June",
  title =   "Plug - in Timing Models for an Abstar"
}

@inproceedings{WaS88,
  author =  "David E. Wallace and Carlo H. S\'e quin",
  booktitle =   "Proceedings of the 25th Design Automation Conference",
  year  =   "1988",
  month =   "June",
  title =   "{ATV:} An Abstract Timing Verifier"
}

@book{DeM94,
  author =  "Giovanni De Micheli",
  year  =   "1994",
  publisher =   "McGraw-Hill",
  title =   "Synthesis and Optimization of Digital Circuits"
}



@inproceedings{KuM90,
  author =  "David Ku and Giovanni De Micheli",
  booktitle =   "Proceedings of the 27th Design Automation Conference",
  year  =   "1990",
  month =   "June",
  pages =   "59--64",
  title =   "Relative Scheduling under Timing Constaints"
}

@incollection{DaR88,
  author =  "Michel R. Dagenais and Nicholas C. Rumin",
  booktitle =   "Advanced Research in VLSI",
  year  =   "1988",
  month =   "March",
  editor =  "Jonathan Allen and F. Thomson Leighton",
  publisher =   "MIT Press",
  pages =   "19--33",
  series =  "Applied Sciences - No. 136",
  title =   "Automatic Determination of Optimal Clocking Parameters in Synchronous {MOS} {VLSI} Circuits"
}

@inproceedings{McWi80,
  author =  "T. M. McWilliams",
  booktitle =   "Proceedings of the 17th Design Automation Conference",
  year  =   "1980",
  month =   "June",
  pages =   "139--147",
  title =   "Verification of Timing Constaints on Large Digital Systems"
}

@article{NoCG92,
  author =  "Stefan Note and Francky Catthoor and Gert Goossens and Hugo J. De Man",
  year  =   "1992",
  month =   "April",
  journal = "IEEE Transactions on Computer-Aided Design",
  number =  "4",
  pages =   "413--423",
  title =   "Combined Hardware Selection and Pipelining in High-Performance Data-Path Design",
  volume =  "11"
}

@article{BreG90,
  author =  "Forrest Brewer and Daniel Gajski",
  year  =   "1990",
  month =   "July",
  journal = "IEEE Transactions on Computer-Aided Design",
  number =  "7",
  pages =   "681--695",
  title =   "Chippe: A System for Constaint Driven Behavioral Synthesis",
  volume =  "9"
}

@inproceedings{PaG87,
  author =  "Barry M. Pangrle and Daniel Gajski",
  booktitle =   "Proceedings of the Int'l Conference on Computer Design",
  year  =   "1987",
  month =   "Oct.",
  pages =   "42--45",
  title =   "Slicer: A State Synthesizer for Intelligent Silicon Compilation"
}

@inproceedings{BoK87,
  author =  "Gaetano Borriello and Randy H. Katz",
  booktitle =   "Int'l Conference on Computer-Aided Design",
  year  =   "1987",
  pages =   "274--277",
  title =   "Synthesis and Optimization of Interface Transducer Logic"
}

@book{ASe86,
  author =  "Alfred V. Aho and Ravi Sethi and Jeffrey D. Ullman",
  year  =   "1986",
  publisher =   "Addison-Wesley Publishing Company",
  title =   "Compilers, Principles, Techniques, and Tools"
}

@article{DBr81,
  author =  "John A. Darringer and Daniel Brand and John V. Gerbi and William H. Joyner and Louise H. Trevillyan",
  year  =   "1981",
  month =   "July",
  journal = "IBM Journal on Research and Development",
  number =  "4",
  pages =   "272--280",
  title =   "Logic Synthesis through Local Transformations",
  volume =  "25"
}

@book{Ho75,
  author =  "Holland, J.",
  year  =   "1975",
  publisher =   "Univ. of Michigan Press",
  title =   "Adaption in Natural and Artificial Systems"
}

@article{BrR87,
  author =  "Robert K. Brayton and Richard Rudell and Alberto Sangiovanni-Vincentelli and Albert R. Wang",
  year  =   "1987",
  month =   "Nov.",
  journal = "IEEE Transactions on Computer-Aided Design",
  number =  "6",
  pages =   "1062--1081",
  title =   "{MIS}: A Multiple-Level Logic Optimization System",
  volume =  "6"
}

@inproceedings{SaW91,
  author =  "Hamid Savoj and Huey-Yih Wang and Robert K. Brayton",
  booktitle =   "Proceedings of the M.C.N.C. Workshop on Logic Synthesis",
  year  =   "1991",
  month =   "April",
  title =   "Improved Scripts in {MIS-II} for Logic Minimization of Combinatorial Circuits"
}

@inproceedings{Pip91,
  author =  "Mauro Pipponzi",
  booktitle =   "Proceedings of the M.C.N.C. Workshop on Logic Synthesis",
  year  =   "1991",
  month =   "April",
  title =   "{MDRIVER}: A Strategy Generation for Multiple-Level Optimization"
}

@article{KiG83,
  author =  "Kirkpatrick, S. and Gelatt, C. D. and Vecchi, M. P.",
  year  =   "1983",
  journal = "Science",
  number =  "220",
  pages =   "671--680",
  title =   "Optimization by Simulated Annealing"
}

@inproceedings{Koz91,
  author =  "John R. Koza",
  booktitle =   "Proceedings of the Fourth Int'l Conference on Genetic Algorithms",
  year  =   "1991",
  month =   "July",
  title =   "Evolving a Computer Program to Genetic Random Numbers Using the Genetic Programming Paradigm"
}

@inbook{Ant91,
  author =  "Hendrik James Antonisse",
  year  =   "1991",
  editor =  "Gregory J. E. Rawlins",
  publisher =   "Morgan Kaufmann Publishers",
  pages =   "193--204",
  title =   "A Grammar-Based Genetic Algorithm"
}

@inproceedings{KuH92,
  author =  "Sandip Kundu and Leendert M. Huisman and Indira Nair and Vijay Ivengar and Lakshmi Reddy",
  booktitle =   "Proceedings of the Int'l Test Conference",
  year  =   "1992",
  pages =   "30--40",
  title =   "A small test generator for large designs"
}

@inproceedings{RaV90,
  author =  "Rajski, I. and Vasudevamurthy, J",
  booktitle =   "Proceedings of the Int'l Test Conference",
  year  =   "1990",
  pages =   "265--273",
  title =   "Testability Preserving Transformations in Multi-level Logic Synthesis"
}

@inproceedings{Che92,
  author =  "Chen, K.-C.",
  booktitle =   "Proceedings of the 29th Design Automation Conference",
  year  =   "1992",
  month =   "June",
  pages =   "443--448",
  title =   "Efficient Sum-To-One Subsets Algorithms for Logic Optimization"
}

@inproceedings{PeB91,
  author =  "Pedram, M. and Bhat, N.",
  booktitle =   "Proceedings of the 28th Design Automation Conference",
  year  =   "1991",
  month =   "June",
  pages =   "99--105",
  title =   "Layout driven technology mapping"
}

@inproceedings{FrR90,
  author =  "Francis, R. J. and Rose, J. and Chung, K.",
  booktitle =   "Proceedings of the 27th Design Automation Conference",
  year  =   "1990",
  month =   "June",
  pages =   "613--619",
  title =   "Chortle: A technology mapping program for lookup table-based field programmable gate arrays"
}

@inproceedings{BeH90,
  author =  "Berman, C. L. and Hathaway, D. J. and LaPaugh, A. S. and Trevillyan, L. H.",
  booktitle =   "Proceedings of the Int'l Symposium on Circuits and Systems",
  year  =   "1990",
  pages =   "415--419",
  title =   "Efficient techniques for timing correction"
}

@inproceedings{ToS91,
  author =  "Touati, H. J. and Savoj, H. and Brayton, R. K.",
  booktitle =   "Int'l Conference on Computer-Aided Design",
  year  =   "1991",
  month =   "Nov.",
  pages =   "188--191",
  title =   "Delay Optimization of Combinatorial Logic Circuits by Clustering and Partial Collapsing"
}

@book{Gol89,
  author =  "Goldberg, D. E.",
  year  =   "1989",
  publisher =   "Addison-Wesley",
  title =   "Genetic Algorithms in Search, Optimization and Machine Learning"
}

@techreport{MCNC91,
  author =  "S. Yang",
  year  =   "1991",
  month =   "Jan.",
  institution = "MCNC Technical Report",
  title =   "Logic Synthesis and Optimization Benchmarks User Guide, Version 3.0"
}

@inproceedings{GiK93,
  author =  "van Ginneken, L. P. P. P. and Kuehlmann, A.",
  booktitle =   "M.C.N.C. Workshop on Logic Synthesis",
  year  =   "1993",
  month =   "May",
  title =   "Tuning of Logic Synthesis Scenarios"
}

@article{Bry86,
  author =  "Randal E. Bryant",
  year  =   "1986",
  month =   "August",
  journal = "IEEE Transactions on Computers",
  pages =   "677--691",
  title =   "Graph-based algorithms for {B}oolean function manipulation",
  number =  "8",
  volume =  "C-35"
}

@inproceedings{JBi91,
  author =  "Jain, J and Bitner, J. and Fussel, D. S. and Abraham, J. A.",
  booktitle =   "Int'l Conference on Computer-Aided Design",
  year  =   "1991",
  month =   "Nov.",
  pages =   "468--471",
  title =   "Probabilistic Design Verification"
}

@article{AFe88,
  author =  "Magdy S. Abadir and Jack Ferguson and Thomas E. Kirkland",
  year  =   "1988",
  month =   "Jan.",
  journal = "IEEE Transactions on Computer-Aided Design",
  number =  "1",
  pages =   "138--148",
  title =   "Logic Design Verification via Test Generation",
  volume =  "7"
}

@inproceedings{ChW93,
  author =  "Pi-Yu Chung and Yi-Min Wang and Ibrahim N. Hajj",
  booktitle =   "Proceedings of the 30th Design Automation Conference",
  year  =   "1993",
  month =   "June",
  pages =   "503--508",
  title =   "Diagnosis and Correction of Logic Errors in Digital Circuits"
}

@inproceedings{PoR93,
  author =  "Irith Pomeranz and Sudhakar M. Reddy",
  booktitle =   "Digest of Technical Papers of the Int'l Conference on Computer-Aided Design",
  year  =   "1993",
  month =   "Nov.",
  pages =   "500--507",
  title =   "On Diagnosis and Correction of Design Errors"
}

@inproceedings{MaC89,
  author =  "Jean Christophe Madre and Oliver Coudert and Jean Paul Billon",
  booktitle =   "Int'l Conference on Computer-Aided Design",
  year  =   "1989",
  month =   "Nov.",
  pages =   "30--33",
  title =   "Automating the Diagnosis and the Rectification of Design Errors with {PRIAM}"
}

@inproceedings{ToJ90,
  author =  "Masahiro Tomita and Hong-Hai Jiang",
  booktitle =   "Int'l Conference on Computer-Aided Design",
  year  =   "1990",
  month =   "Nov.",
  pages =   "468--471",
  title =   "An Algorithm for Locating Logic Design Errors"
}

@inproceedings{Ru93,
  author =  "Richard Rudell",
  booktitle =   "Int'l Workshop on Logic \& Synthesis",
  year  =   "1993",
  month =   "May",
  title =   "Dynamic Variable Ordering for Ordered Binary Decision Diagrams"
}
%  pages =  "3a-1--3a-12",


@inproceedings{BRy93,
  author =  "Randal E. Bryant",
  booktitle =   "Int'l Conference on Computer-Aided Design",
  year  =   "1991",
  month =   "Nov.",
  pages =       "350--353",
  title =   "Extraction of Gate Level Models from Transistor Circuits by Four-Valued Symbolic Analysis"
}

@article{BRy87,
  author =  "Randal E. Bryant",
  year  =   "1987",
  month =   "July",
  journal = "IEEE Transactions on Computer-Aided Design",
  number =  "4",
  pages =   "634--649",
  title =   "{B}oolean Analysis of {MOS} Circuits",
  volume =  "6"
}

@inproceedings{BlS91,
  author =  "D. T. Blaauw and D. G. Saab and P. Banerjee and J. A. Abraham",
  booktitle = "Proceedings of The European Conference on Design Automation",
  year  =   "1991",
  month =   "February",
  publisher =   "IEEE",
  pages =   "329--333",
  title =   "Functional Abstraction of Logic Gates for Switch-Level Simulation"
}

@article{CoR88,
  author =  "Henry Cox and Janusz Rajski",
  year  =   "1988",
  month =   "July",
  journal = "IEEE Transactions on Computer-Aided Design",
  number =  "7",
  pages =   "813--833",
  title =   "A Method of Fault Analysis for Test Generation and Fault Diagnosis",
  volume =  "7"
}

@inproceedings{LiT90,
  author =  "Heh-Tyan Liaw and Jia-Horng Tsaih and Cheng-Shang Lin",
  booktitle = "Int'l Conference on Computer-Aided Design",
  year  =   "1990",
  month =   "Nov.",
  pages =   "464--467",
  title =   "Efficient Automatic Diagnosis of Digital Circuits"
}

@article{AwL89,
  author =  "John A. Waicukauski and Eric Lindblom",
  year  =   "1989",
  month =   "August",
  journal = "IEEE Design \& Test of Computers",
  pages =   "49--60",
  title =   "Failure Diagnosis of Structured {VLSI}"
}

@inproceedings{DiD83,
  author =  "G. Ditlow and W. Donath and A. Ruehli",
  booktitle =   "Proceedings of the Int'l Symposium on Circuits and Systems",
  year  =   "1983",
  month =   "May",
  pages =   "752--755",
  title =   "Logic Equations for {MOSFET} Circuits"
}

@inproceedings{BeBr88,
  author =  "Derek L. Beatty and Randal E. Bryant",
  booktitle =   "Proceedings of the 25th Design Automation Conference",
  year  =   "1988",
  month =   "June",
  pages =   "495--500",
  title =   "Fast Incremental Circuit Analysis Using Extracted Hierarchy"
}

@book{Hu65,
  author =  "Sze-Tsen Hu",
  year  =   "1965",
  publisher =   "University of California Press",
  title =   "Threshold Logic"
}

@phdthesis{Ra92,
  author =  "Werner De Rammelaere",
  year  =   "1992",
  month =   "June",
  school =  "Katholieke Universiteit Leuven",
  title =   "Static Electrical Verification of Synchronous Digital {MOS} Circuits"
}

@phdthesis{Lo93,
  author =  "David E. Long",
  school =  "Carnegie Mellon University",
  year  =   "1993",
  month =   "July",
  title =   "Model Checking, Abstraction and Compositional Verification"
}



@article{SmBH82,
  author =  "Gordon L. Smith and Ralph J. Bahnsen and Harry Halliwell",
  year  =   "1982",
  month =   "Jan.",
  journal = "IBM Journal of Research and Development",
  number =  "1",
  pages =   "106--116",
  title =   "{B}oolean Comparison of Hardware and Flowcharts",
  volume =  "26"
}

@article{Mo82,
  author =  "Michael Monachino",
  year  =   "1982",
  month =   "Jan.",
  journal = "IBM Journal of Research and Development",
  number =  "1",
  pages =   "89--99",
  title =   "Design Verification System for Large-Scale {LSI} Designs",
  volume =  "26"
}

@article{Rot77,
  author =  "J. Paul Roth",
  year  =   "1977",
  month =   "Dec.",
  journal = "IEEE Transactions on Computers",
  number =  "12",
  pages =   "1292--1294",
  title =   "Hardware Verification",
  volume =  "C-26"
}

@article{Rot66,
  author =  "J. Paul Roth",
  year  =   "1966",
  month =   "July",
  journal = "IBM Journal of Research and Development",
  pages =   "278--291",
  title =   "Diagnosis of Automata Failures: A Calculus \& Method",
  volume =  "10"
}

@incollection{CaG87,
  author =  "A. Camilleri and M. Gordon and T. Melham",
  booktitle =   "From {HDL} Descriptions to Guaranteed Correct Circuit Designs",
  year  =   "1987",
  title =   "Hardware verification using high-order logic"
}

@inproceedings{HaD85,
  author =  "F. K. Hanna and N. Daeche",
  booktitle =   "Proceedings of 7th CHDL",
  year  =   "1985",
  title =   "Specification and verification using higher-order logic"
}

@inproceedings{DeT87,
  author =  "Srinivas Devadas and Hi-Keung Tony Ma and A. Richard Newton",
  booktitle =   "Proceedings of the 24th Design Automation Conference",
  year  =   "1987",
  pages =   "271--276",
  title =   "On the Verification of Sequential Machines at Different Levels of Abstraction"
}


@article{BuCL94,
  author =  "J. R. Burch and E. M. Clarke and D. E. Long and K. L. McMillan and D. L. Dill",
  year  =   "1994",
  month =   "April",
  journal = "IEEE Transactions on Computer-Aided Design",
  number =  "4",
  pages =   "401--424",
  title =   "Symbolic Model Checking for Sequential Circuit Verification",
  volume =  "13"
}

@article{JaGa94,
  author =  "P. Jain and Ganesh Gopalakrishnan",
  year  =   "1994",
  month =   "April",
  journal = "IEEE Transactions on Computer-Aided Design",
  number =  "8",
  pages =   "1005--1015",
  title =   "Efficient Symbolic Simulation-Based Verification Using the Parametric Form of {B}oolean Expressions",
  volume =  "13"
}

@inproceedings{BuCM90,
  author =  "J. R. Burch and E. M. Clarke and K. L. McMillan and D. L. Dill and L. J. Hwang",
  year  =   "1990",
  month =   "June",
  booktitle =   "Fifth Annual Symposium on Logic in Computer Science",
  title =   "Symbolic Model Checking: $10^{20}$ States and Beyond"
}
%  pages =   "428--439",

@inproceedings{ClLoMc89,
  author =  "Edmund M. Clarke and David E. Long and Kenneth L. McMillan",
  year  =   "1989",
  month =   "June",
  booktitle =   "IEEE Symposium on Logic in Computer Science",
  pages =   "353--362",
  title =   "Compositional Model Checking"
}


@article{DaB85,
  author =  "W. J. Dally and R. E. Bryant",
  year  =   "1985",
  month =   "July",
  journal = "IEEE Transactions on Computer-Aided Design",
  number =  "3",
  pages =   "239--249",
  title =   "A Hardware Architecture for Switch-Level Simulation",
  volume =  "4"
}

@inproceedings{Fra85,
  author =  "E. H. Frank",
  booktitle =   "Proceedings of the 22rd Design Automation Conference",
  year  =   "1985",
  month =   "June",
  pages =   "735--738",
  title =   "Switch-Level Simulation of {VLSI} using special-purpose, data-driven computer"
}

@inproceedings{Bar83,
  author =  "Z. Barzilai and L. M. Huisman and G. M. Silberman and D. T. Tang and L. S. Woo",
  booktitle =   "Proceedings of the 20th Design Automation Conference",
  year  =   "1983",
  month =   "June",
  pages =   "157--163",
  title =   "Simulating Pass Transistor Circuits Using Logic Simulation Machines"
}

@inproceedings{Den82,
  author =  "M. M. Denneau",
  booktitle =   "Proceedings of the 19th Design Automation Conference",
  year  =   "1982",
  month =   "June",
  pages =   "55--59",
  title =   "The {Y}orktown Simulation Engine"
}

@inproceedings{RUd93a,
  author =  "Richard Rudell",
  booktitle =   "Digest of Technical Papers of the Int'l Conference on Computer-Aided Design",
  year  =   "1993",
  month =   "Nov.",
  pages =   "42--47",
  title =   "Dynamic Variable Ordering for Ordered Binary Decision Diagrams"
}

@inproceedings{ShD93,
  author =  "A. Shen and S. Devadas and A. Ghosh",
  booktitle =   "Digest of Technical Papers of the Int'l Conference on Computer-Aided Design",
  year  =   "1993",
  month =   "Nov.",
  pages =   "544--549",
  title =   "Probabilistic Construction and Manipulation of Free {B}oolean Diagrams"
}

@inproceedings{Bra93,
  author =  "Daniel Brand",
  booktitle =   "Digest of Technical Papers of the Int'l Conference on Computer-Aided Design",
  year  =   "1993",
  month =   "Nov.",
  pages =   "534--537",
  title =   "Verification of Large Synthesized Designs"
}

@inproceedings{Kun93,
  author =  "Wolfgang Kunz",
  booktitle =   "Digest of Technical Papers of the Int'l Conference on Computer-Aided Design",
  year  =   "1993",
  month =   "Nov.",
  pages =   "538--543",
  title =   "{HANNIBAL:} {A}n Efficient Tool for Logic Verification Based on Recursive Learning"
}

@article{FuF93,
  author =  "M. Fujita and H. Fujisawa and Y. Matsunaga",
  year  =   "1993",
  month =   "Jan.",
  journal = "IEEE Transactions on Computer-Aided Design",
  number =  "1",
  pages =   "6--12",
  title =   "Variable Ordering Algorithms for Ordered Binary Decision Diagrams and their Evaluation",
  volume =  "12"
}

@article{Ake78,
  author =  "Sheldon B. Akers",
  year  =   "1978",
  month =   "June",
  journal = "IEEE Transactions on Computers",
  number =  "6",
  pages =   "509--516",
  title =   "Binary Decision Diagrams",
  volume =  "27"
}

@article{Bry84,
  author =  "Randal E. Bryant",
  year  =   "1984",
  month =   "February",
  journal = "IEEE Transactions on Computers",
  number =  "2",
  pages =   "160--177",
  title =   "A Switch-Level Model and Simulator for {MOS} Digital Systems",
  volume =  "33"
}

@article{Far93,
  author =  "Michael C. McFarland",
  year  =   "1993",
  month =   "May",
  journal = "IEEE Transactions on Computer-Aided Design",
  number =  "5",
  pages =   "633--653",
  title =   "Formal Verification of Sequential Hardware: A Tutorial",
  volume =  "12"
}

@article{Gup92,
  author =  "Aarti Gupta",
  year  =   "1992",
  publisher =   "Kluwer Academic Publisher",
  journal = "Formal Methods in System Design",
  number =  "1",
  pages =   "5--92",
  title =   "Formal Hardware Verification Methods: A Survey"
}

@article{AsDeKe93,
  author =  "Pranav Ashar and Srinivas Devadas and Kurt Keutzer",
  year  =   "1993",
  publisher =   "Kluwer Academic Publisher",
  journal = "Formal Methods in System Design",
  number =  "1",
 volume =   "2",
  pages =   "93--112",
  title =   "Gate-Delay-Fault Testability Properties of Multiplexor-Based Networks"
}

@techreport{KuCh93,
  author =  "A. Kuehlmann and D. I. Cheng and A. Srinivasan and D. P. LaPotin",
  year  =   "1993",
  month =   "Oct.",
  number =  "Computer Science, RC 19219 (\#83668)",
  institution = "IBM Research Division, T. J. Watson Research Center, Yorktown Heights, NY 10598",
  title =   "Error Diagnosis for Transistor-Level Verification"
}

@inproceedings{KuCh94,
  author =  "A. Kuehlmann and D. I. Cheng and A. Srinivasan and D. P. {LaPotin}",
  booktitle =   "Proceedings of the 31th Design Automation Conference",
  year  =   "1994",
  month =   "June",
  pages =   "218--224",
  title =   "Error Diagnosis for Transistor-Level Verification",
  ftp =     "http://blankenburg.watson.ibm.com:8001/ps/dac94.ps.Z",
  html =    "http://blankenburg.watson.ibm.com:8001/html/dac94/dac94.html"
}

@article{KuSr95,
  author =  "Andreas Kuehlmann and Arvind Srinivasan and David P. {LaPotin}",
  year  =   "1995",
  month =   "Jan./March",
  journal = "IBM Journal of Research and Development",
  number =  "1/2",
  pages =   "149--165",
  title =   "Verity - a formal verification program for custom {CMOS} circuits",
  volume =  "39",
  ftp =     "http://blankenburg.watson.ibm.com:8001/ps/ibm94.ps.Z",
  html =    "http://blankenburg.watson.ibm.com:8001/html/ibm94/ibm94.html"
}

@inproceedings{KaS92,
  author =  "Timothy Kam and P. A. Subrahmanyam",
  booktitle =   "Proceedings of the Int'l Conference on Computer Design",
  year  =   "1992",
  month =   "Oct.",
  pages =   "588--591",
  title =   "Comparing Layouts with {HDL} Models: A Formal Verification Technique"
}

@inproceedings{BrD87,
  author =  "Randal E. Bryant and Derek Beatty and Karl Brace",
  booktitle =   "Proceedings of the 24th Design Automation Conference",
  year  =   "1987",
  pages =   "9--16",
  title =   "{COSMOS:} A Compiled Simulator for {MOS} Circuits"
}

@inproceedings{JaB91,
  author =  "Alok Jain and Randal E. Bryant",
  booktitle =   "Proceedings of the 28th Design Automation Conference",
  year  =   "1991",
  month =   "June",
  pages =   "219--222",
  title =   "Mapping switch-level simulation onto gate-level hardware accelerators"
}

@book{MeC80,
  author =  "Carver Mead and Lynn Conway",
  year  =   "1980",
  publisher =   "Addison-Wesley Publishing Company",
  title =   "Introduction to {VLSI} Systems"
}

@article{Kau70,
  author =  "W. H. Kauz",
  year  =   "1970",
  month =   "February",
  journal = "IEEE Transactions on Computers",
  pages =   "162--164",
  title =   "The necessity of closed loops in minimal combinational circuits"
}

@inproceedings{Mal93,
  author =  "Sharad Malik",
  booktitle =   "Digest of Technical Papers of the Int'l Conference on Computer-Aided Design",
  year  =   "1993",
  month =   "Nov.",
  pages =   "618--625",
  title =   "Analysis of Cyclic Combinatorial Circuits"
}

@inproceedings{Ebe88,
  author =  "Carl Ebeling",
  booktitle =   "Int'l Conference on Computer-Aided Design",
  year  =   "1988",
  month =   "Nov.",
  pages =   "322--325",
  title =   "Gemini{II}: A Second Generation Layout Validation Program"
}

@book{McM93,
  author =  "Kenneth L. McMillan",
  year  =   "1993",
  publisher =   "Kluwer Academic Publishers",
  title =   "Symbolic Model Checking"
}

@inproceedings{BeD90,
  author =  "D. K. Beece and R. Damiano and G. Papp and R. Schoen",
  booktitle =   "Proceedings of The European Conference on Design Automation",
  year  =   "1990",
  month =   "March",
  publisher =   "IEEE",
  pages =   "290--295",
  title =   "The {EVE} Companion Simulator"
}

@techreport{KuG93,
  author =  "Kuehlmann, A. and van Ginneken, L. P. P. P.",
  year  =   "1993",
  month =   "March",
  number =  "Computer Science, RC  18838 (\#82376)",
  institution = "IBM Research Division, T. J. Watson Research Center, Yorktown Heights, NY 10598",
  title =   "Grammar-Based Optimization of Synthesis Scenarios"
}

@article{BlC80,
  author =  "M. Blum and A. K. Chandra and M. N. Wegman",
  year  =   "1980",
  month =   "March",
  journal = "Information Processing Letters",
  number =  "2",
  pages =   "80--82",
  title =   "Equivalence of Free {B}oolean Graphs can be Decided Probabilistically in Polynomial Time",
  volume =  "10"
}

@inproceedings{MaB88,
  author =  "Jean-Christophe Madre and Jean-Paul Billon",
  booktitle =   "Proceedings of the 25th Design Automation Conference",
  year  =   "1988",
  month =   "June",
  pages =   "205--210",
  title =   "Proving Circuit Correctness using Formal Comparison Between Expected and Extracted Behaviour"
}

@inproceedings{GeC92,
  author =  "Mark Genoe and Luc Claesen and Eric Verlind and Frank
                 Proesmans and Hugo De Man",
  booktitle =   "Proceedings of The European Conference on Design Automation",
  year  =   "1992",
  month =   "February",
  publisher =   "IEEE",
  pages =   "54--58",
  title =   "Automatic Formal Verification of {Cathedral-II}
          Circuits from Transistor Switch Level
          Implementations up to High Level Behavioral
          Specifications by the {SFG}-Tracing Methodology"
}

@InProceedings{goldberg02berkmin,
  author = "E. Goldberg and Y. Novikov",
  title = "BerkMin: A Fast and Robust SAT Solver",
  booktitle =    date, 
  year =         2002,
}
%, pp. 142-149.",

@misc{KueSom95,
  author =  "Andreas Kuehlmann and David P. {LaPotin}",
  year  =   "1995",
  month =   "Jan.",
  title =   "{VERITY} - Verification of Custom CMOS Microprocessors",
  note =        "Slides of the presentation at the Somerset Design Center",
  ftp =     "http://blankenburg.watson.ibm.com:8001/ps/verity1_95.ps.Z"
}

@techreport{ApKu95,
  author =  "David P. Appenzeller and A. Kuehlmann",
  year  =   "1995",
  month =   "March",
  number =  "Computer Science, RC 19971 (\#88427)",
  institution = "IBM Research Division, T. J. Watson Research Center, Yorktown Heights, NY 10598",
  title =   "Formal Verification of a {PowerPC} Microprocessor",
  ftp =     "http://blankenburg.watson.ibm.com:8001/ps/iccd95.ps.Z",
  html =    "http://blankenburg.watson.ibm.com:8001/html/iccd95/iccd95.html"
}

@techreport{Met95,
  author =  "Arjen Mets",
  year  =   "1995",
  month =   "Jan.",
  number =  "Computer Science, RC 19894 (\#88043)",
  institution = "IBM Research Division, T. J. Watson Research Center, Yorktown Heights, NY 10598",
  title =   "Formal Verification of Sequential Circuits Using
             Implicit State Enumeration",
  ftp =     "http://blankenburg.watson.ibm.com:8001/ps/seq.ps.Z",
  html =    "http://blankenburg.watson.ibm.com:8001/html/seq.html"
}

@inproceedings{ApKu95a,
  author =  "David P. Appenzeller and A. Kuehlmann",
  booktitle =   "Proceedings of the Int'l Conference on Computer Design",
  year  =   "1995",
  month =   "Oct.",
  pages =   "79--84",
  title =   "Formal Verification of a {PowerPC} Microprocessor"
}

@inproceedings{ChHa93,
  author =  "Hyunwoo Cho and Gary D. Hachtel and Enrico Macii and
          Bernard Plessier and Fabio Somenzi",
  booktitle =   "Proceedings of the 30th Design Automation Conference",
  year  =   "1993",
  month =   "June",
  pages =   "25--30",
  title =   "Algorithms for Approximate {FSM} Traversal"
}

@inproceedings{CoB89,
  author =  "O. Coudert and C. Berthet and J. C. Madre",
  booktitle =   "IMEC-IFIP Int'l Workshop on Applied Formal Methods for Correct VLSI Design",
  year  =   "1989",
  month =   "Nov.",
  pages =   "111--128",
  title =   "Verification of Sequential Machines Using {B}oolean Functional Vectors"
}

@inproceedings{CoB89a,
  author =  "O. Coudert and C. Berthet and J. C. Madre",
  booktitle =   "Int'l Workshop on Automatic Verification Methods for Finite State Systems",
  year  =   "1989",
  month =   "June",
  pages =   "365--373",
  title =   "Verification of Synchronous Sequential Machines Based on Symbolic Execution"
}

@inproceedings{CaCa94,
  author =  "Gianpiero Cabodi and Paolo Camurati and Stefano Quer",
  booktitle =   "Proceedings of the Int'l Conference on Computer Design",
  year  =   "1994",
  month =   "Oct.",
  pages =   "230--239",
  title =   "Efficient State Space Pruning in Symbolic Backward Traversal"
}

@inproceedings{AzSSB94,
  author =  "Adnan Aziz and Vigyan Singhal and Gitanjali Swamy and Robert Brayton",
  booktitle =   "International Conference on Computer Design",
  year  =   "1994",
  month =   "Oct.",
  title =   "Minimizing Interacting Finite State Machines: A Compositional Approach to Language Containment"
}
%  pages =  "255--261",


@inproceedings{ChHa90,
  author =  "Hyunwoo Cho and Gary D. Hachtel and Seh-Woong Jeong  and Bernard Plessier
          and Eric Schwarz and Fabio Somenzi",
  booktitle =   "Int'l Conference on Computer-Aided Design",
  year  =   "1990",
  month =   "Nov.",
  pages =   "134--137",
  title =   "{ATPG} Aspects of {FSM} Verification"
}


@inproceedings{ToSa90,
  author =  "H. J. Touati and H. Savoj and B. Lin and
          R. K. Brayton and A. Sangiovanni-Vincentelli",
  booktitle =   "Int'l Conference on Computer-Aided Design",
  year  =   "1990",
  month =   "Nov.",
  pages =   "130--133",
  title =   "Implicit State Enumeration for Finite State Machines using {BDD}'s"
}

@inproceedings{CoMa90,
  author =  "O. Coudert and J. C. Madre",
  booktitle =   "Int'l Conference on Computer-Aided Design",
  year  =   "1990",
  month =   "Nov.",
  pages =   "126--129",
  title =   "A Unified Framework for the Formal Verification of Sequential Circuits"
}

@inproceedings{Fil91,
  author =  "Thomas Filkorn",
  booktitle =   "Proceedings of 10th IFIP Symposium on Computer
          Hardware Description Languages (CHDL'91)",
  year  =   "1991",
  title =   "A Method for Symbolic Verification of Synchronous Circuits"
}


@inproceedings{BeTr89,
  author =  "C. Leonard Berman and Louise H Trevillyan",
  booktitle =   "Int'l Conference on Computer-Aided Design",
  year  =   "1989",
  month =   "Nov.",
  pages =   "456--459",
  title =   "Functional Comparison of Logic Designs for {VLSI} Circuits"
}

@inproceedings{EiJe95,
  author =  "C. A. J. van Eijk and J. A. G. Jess",
  booktitle =   "1995 Int'l Workshop on Logic \& Synthesis",
  year  =   "1995",
  month =   "May",
  pages =   "3-35 -- 3-44",
  title =   "Detection of Equivalent State Variables in Finite
             State Machine Verification"
}

@inproceedings{BrRu87,
  author =  "Karl S. Brace and Richard L. Rudell and Randal E. Bryant",
  booktitle =   "Proceedings of the 27th Design Automation Conference",
  year  =   "1990",
  month =   "June",
  pages =   "40--45",
  title =   "Efficient Implementation of a {BDD} Package"
}

@inproceedings{JaMu95,
  author =  "Jawahar Jain and Rajarshi Mukherjee and Masahiro Fujita",
  booktitle =   "Proceedings of the 32th Design Automation Conference",
  year  =   "1995",
  month =   "June",
  pages =   "420--426",
  title =   "Advanced Verification Technique Based on Learning"
}

@inproceedings{ReKu95,
  author =  "Subodh M. Reddy and Wolfgang Kunz and Dhiraj K. Pradhan",
  booktitle =   "Proceedings of the 32th Design Automation Conference",
  year  =   "1995",
  month =   "June",
  pages =   "414--419",
  title =   "Novel Verification Framework Combining Structural and
                 {OBDD} Methods in a Synthesis Environment"
}

@inproceedings{Mats96,
  author =  "Yusuke Matsunaga",
  booktitle =   "Proceedings of the 33th Design Automation Conference",
  year  =   "1996",
  month =   "June",
  pages =   "629--634",
  title =   "An Efficient Equivalence Checker for Combinatorial Circuits"
}

@inproceedings{EiJa95,
  author =  "C.A.J. van Eijk and G.L.J.M. Janssen",
  booktitle =   "Proceedings of the 2nd Int'l Conference on
                 Theorem Provers in Circuit Design",
  year  =   "1995",
  pages =   "110--125",
  title =   "Exploiting Structural Similarities in a {BDD}-based Verification Method"
}

@inproceedings{KrKu96,
  author =  "Florian Krohm and Andreas Kuehlmann and Arjen Mets",
  booktitle =   "Int'l Conference on Computer Design",
  year  =   "1996",
  month =   "Oct.",
  pages =   "371--376",
  title =   "The Use of Random Simulation in Formal Verification"
}

@inproceedings{PaJa95,
  author =  "Manish Pandey and Alok Jain and Randal E. Bryant and
                 Derek Beatty and Gary York and Samir Jain",
  booktitle =   "Proceedings of the Int'l Conference on Computer Design",
  year  =   "1995",
  month =   "Oct.",
  pages =   "596--601",
  title =   "Extraction of Finite State Machines from Transistor
                 Netlists by Symbolic Simulation"
}

@inproceedings{JaBr95,
  author =  "Samir Jain and Randal E. Bryant and Alok Jain",
  booktitle =   "Proceedings of the 32nd Design Automation Conference",
  year  =   "1995",
  month =   "June",
  pages =   "707--711",
  title =   "Automatic Clock Abstraction from Sequential Circuits"
}

@article{RaBi93,
  author =  "Rahul Razdan and Gabriel P. Bischoff and Ernst G. Ulrich",
  year  =   "1993",
  month =   "Oct.",
  journal = "IEEE Transactions on Computer-Aided Design",
  number =  "10",
  pages =   "1547--1556",
  title =   "Clock Suppression Techniques for Synchronous Circuits",
  volume =  "12"
}

@inproceedings{KuKr97,
  author =  "Andreas Kuehlmann and Florian Krohm",
  booktitle =   "Design Automation Conference",
  year  =   "1997",
  month =   "June",
  pages =   "263--268",
  title =   "Equivalence Checking using Cuts and Heaps"
}

@inproceedings{BuSi98,
  author =  "Jerry R. Burch and Vigyan Singhal",
  booktitle =   "Digest of Technical Papers of the Int'l Conference on Computer-Aided Design",
  year  =   "1998",
  month =   "Nov.",
  pages =   "570--576",
  title =   "Tight Integration of Combinational Verification Methods"
}

@inproceedings{MoJHSYP98,
  author =  "In-Ho Moon and Jae-Young Jang and Gary D. Hachtel and Fabio Somenzi and Jun Yuan and Carl Pixley",
  booktitle =   "Int'l Conference on Computer-Aided Design",
  year  =   "1998",
  month =   "Nov.",
  pages =   "351--358",
  title =   "Approximate reachability don't cares for {CTL} model checking"
}

@inproceedings{BuSi98a,
  author =  "Jerry R. Burch and Vigyan Singhal",
  booktitle =   "Digest of Technical Papers of the Int'l Conference on Computer-Aided Design",
  year  =   "1998",
  month =   "Nov.",
  pages =   "563--569",
  title =   "Robust Latch Mapping for Combinational Equivalence Checking"
}

@article{KuPr93,
  author =      "W. Kunz and D.K. Pradhan",
  year  =       "1993",
  month =       "May",
  journal =     "IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems",
  number =      "5",
  pages =       "684--694",
  title =       "Recursive learning: a new implication technique for efficient solutions to CAD problems-test, verification, and optimization",
  volume =      "125"
}

@article{DaPu60,
  author =  "Martin Davis and Hilary Putnam",
  year  =   "1960",
  journal = "Journal of of the Association of for Computing Machinery",
  volume =      "7",
  pages =   "102--215",
  title =   "A Computing Procedure for Quantification Theory"
}

@article{DaLL62,
  author =  "Martin Davis and George Logeman and Donald Loveland",
  year  =   "1962",
  journal = "Communications of the ACM",
  volume =      "5",
  pages =   "394--397",
  month =       "July",
  title =   "A Machine Program for Theorem Proving"
}



@inproceedings{JeP91,
  author =      "Seh-Woong Jeong and Bernard Plessier and Gary D. Hachtel and Fabio Somenzi",
  title =       "Extended {BDD}'s: Trading off canonicity for structure in verification algorithms",
  booktitle =   "Int'l Conference on Computer-Aided Design",
  year  =   "1991",
  month =   "Nov.",
  pages =   "464-467"
}

@inproceedings{GuP98,
  author =      "Aarti Gupta and Pranav Ashar",
  title =       "Integrating a {B}oolean Satisfiability Checker and {BDD}s for Combinational Equivalence Checking",
  booktitle =   "Proceedings of the Int'l Conference on VLSI Design",
  pages =       "222--225",
  year  =   "1998"
}

@inproceedings{PaK00,
  author =  "Viresh Paruthi and Andreas Kuehlmann",
  year  =   "2000",
  booktitle =   "Proceedings of the Int'l Conference on Computer Design",
  month =   "Sept.",
  pages =   "459--464",
  title =   "Equivalence Checking Combining a Structural {SAT}-Solver, {BDD}s, and Simulation"
}

@inproceedings{MnSa03,
  author =      "Maher N. Mneimneh and Karem A. Sakallah",
  title =       "{SAT}-based sequential depth computation",
  year  =   "2003",
  month =       "January",
  booktitle =   "ASP Design Automation Conference",
  pages =   "87--92",
}

@article{SiSa99,
  author =      "Jo{\~a}o P. Marques-Silva and Karem A. Sakallah",
  title =       "{GRASP}: a search algorithm for propositional satisfiability",
  year  =   "1999",
  journal = "IEEE Transactions on Computers",
  number =  "5",
  pages =   "506--521",
  volume =  "48"
}

@article{HuWA99,
  author =  "Henrik Hulgaard and Poul F. Williams and Henrik R. Andersen",
  year  =   "1999",
  month =   "July",
  journal = "IEEE Transactions on Computer-Aided Design",
  number =  "7",
  title =   "Equivalence checking of combinational circuits using {B}oolean expression diagrams",
  volume =  "18"
}

@article{LeSa91,
  author =      "C. Leiserson and J. Saxe",
  title =       "Retiming Synchronous Circuitry",
  journal =     "Algorithmica",
  year  =   "1991",
  volume =  "6",
  pages =   "5--35"
}

@article{LeSa83,
  author =  "C. Leiserson and J. Saxe",
  year  =   "1983",
  month =   "Jan.",
  publisher =   "Computer Science Press",
  journal = "Journal of VLSI and Computer Systems",
  number =  "1",
  pages =   "41--67",
  title =   "Optimizing Synchronous Systems",
  volume =  "1"
}

@inproceedings{CaSS00,
  author =  "Gianpiero Cabodi and Stefano Quer and Fabio Somenzi",
  booktitle =   "Design Automation Conference",
  year  =   "2000",
  month =   "June",
  pages =   "601--606",
  title =   "Optimizing Sequential Verification by Retiming Transformations"
}

@inproceedings{GuAM99,
  author =  "Aarti Gupta and Pranav Ashar and Sharad Malik",
  booktitle =   "Correct Hardware Design and Verification Methods",
  year  =   "1999",
  month =   "Sept.",
  pages =   "350--353",
  title =   "Exploiting Retiming in a Guided Simulation Based Validation Methodology"
}

@inproceedings{FiVa99,
  author =  "Kathy Fisler and Moshe Vardi",
  booktitle =   "Correct Hardware Design and Verification Methods",
  year  =   "1999",
  month =   "Sept.",
  pages =   "338--341",
  title =   "Bisimulation and Model Checking"
}

@inproceedings{BaTASA00,
  author =  "Jason Baumgartner and Anson Tripp and Adnan Aziz and Vigyan Singhal and  Flemming Andersen",
  booktitle =   "Computer-Aided Verification",
  year  =   "2000",
  month =   "July",
  pages =   "5--19",
  title =   "An Abstraction Algorithm for the Verification of Generalized {C}-Slow Designs"
}

@inproceedings{NaKu00,
  author =  "Kedar S. Namjoshi and Robert P. Kurshan",
  booktitle =   "Computer-Aided Verification",
  year  =   "2000",
  month =   "July",
  pages =   "435--449",
  title =   "Syntactic Program Transformations for Automatic Abstraction"
}


@inproceedings{KuSh00,
  author =  "James H. Kukula and Thomas R. Shiple",
  booktitle =   "Computer-Aided Verification",
  year  =   "2000",
  month =   "July",
  pages =   "113--123",
  title =   "Building Circuits from Relations"
}

@inproceedings{BaHSA99,
  author =  "Jason Baumgartner and Tamir Heyman and Vigyan Singhal and Adnan Aziz",
  booktitle =   "Computer-Aided Verification",
  year  =   "1999",
  month =   "July",
  pages =   "72--83",
  title =   "Model Checking the {IBM} {G}igahertz {P}rocessor: An Abstraction Algorithm for High-Performance Netlists"
}

@article{MaSB91,
  author =  "Sharad Malik and Ellen M. Sentovich and Robert K. Brayton and Alberto Sangiovanni-Vincentelli",
  year  =   "1991",
  month =   "Jan.",
  journal = "IEEE Transactions on Computer-Aided Design",
  number =  "1",
  pages =   "74--84",
  title =   "Retiming and Resynthesis: Optimizing Sequential Net\-works with Combinational Techniques",
  volume =  "10"
}

@article{ToBr93,
  author =  "Herve J. Touati and Robert K. Brayton",
  year  =   "1993",
  month =   "Jan.",
  journal = "IEEE Transactions on Computer-Aided Design",
  number =  "1",
  pages =   "157--162",
  title =   "Computing the Initial States of Retimed Circuits",
  volume =  "12"
}

@inproceedings{NiPa91,
  author =  "Thomas Niermann and Janak H. Patel",
  booktitle =   "European Conference on Design Automation",
  year  =   "1991",
  month =   "February",
  pages =   "214--218",
  title =   "{HITEC}: A Test Generation Package for Sequential Circuits"
}

@article{EvSS96,
  author =  "Guy Even and Ilan Y. Spillinger and Leon Stok",
  year  =   "1996",
  month =   "March",
  journal = "IEEE Transactions on Computer-Aided Design",
  number =  "3",
  pages =   "348--357",
  title =   "Retiming Revisited and Reversed",
  volume =  "15"
}

@inproceedings{HaMB98,
  author =  "Gagan Hasteer and Anmol Mathur and Prithviraj Banerjee",
  booktitle =   "Int'l Conference on Computer-Aided Design",
  year  =   "1998",
  month =   "Nov.",
  pages =   "557--562",
  title =   "Efficient Equivalence Checking of Multi-Phase Designs Using Retiming"
}

@book{Fil92,
  author =  "Thomas Filkorn",
  year  =   "1992",
  publisher =   "Dissertation, Technische Universit{\"a}t M{\"u}nchen",
  title =   "Symbolische Methoden f{\"u}r die Verifikation endlicher Zustandssysteme"
}

@book{HuRW93,
  author =  "Ming S. Hung and Walter O. Rom and Allan D. Waren",
  year  =   "1993",
  publisher =   "Scientific Press",
  title =   "Optimization with {IBM OSL}"
}
%  author =  "Robert K. Brayton and Gary D. Hachtel and Alberto
%Sangiovanni-Vincentelli and Fabio Somenzi and Adnan Aziz and
%Szu-Tsung Cheng and Stephen Edwards and Sunil Khatri and Yuji
%Kukimoto and Abelardo Pardo and Shaz Qadeer and Rajeev K. Ranjan and
%Shaker Sarwary and Thomas R. Shiple and Gitanjali Swamy and Tiziano Villa",

@inproceedings{VIS96,
  author =  "\mbox{R.~K.~Brayton} et al.",
  booktitle =   "Computer-Aided Verification",
  year  =   "1996",
  month =   "July",
  title =   "{VIS}: A System for Verification and Synthesis"
}
%  pages =   "428--432",


@inproceedings{GaKu00a,
  author =  "Malay Ganai and Andreas Kuehlmann",
  year  =   "2000",
  title =   "On-the-Fly Compression of Logical Circuits",
  month =   "May",
  booktitle =   "Int'l Workshop on Logic \& Synthesis",
}

@article{Eijk00,
  author =  "CAJ van Eijk",
  year  =   "2000",
  month =   "July",
  journal = "IEEE Transactions on Computer-Aided Design",
  number =  "7",
  pages =   "",
  title =   "Sequential equivalence checking based on structural similarities",
  volume =  "19"
}

@inproceedings{KuMP01,
  author =  "Andreas Kuehlmann and Malay Ganai and Viresh Paruthi",
  booktitle =   "Design Automation Conference",
  year  =   "2001",
  month =   "June",
  pages =   "232--237",
  title =   "Circuit-based {B}oolean Reasoning"
}

@inproceedings{MoMZ01,
  author =  "Matthew W. Moskewicz and Conor F. Madigan and Ying Zhao and Linto Zhang and Sharad Malik",
  booktitle =   "ACM Design Automation Conference",
  year  =   "2001",
  month =   "June",
  title =   "Chaff: Engineering an Efficient {SAT} Solver"
}
% pages =   "530--535",

@article{HuCC00,
  author =  "Shi-Yu Huang and Kwang-Ting Cheng and Kuang-Chien Chen and Chung-Yang Huang and  F. Brewer",
  year  =   "2000",
  month =   "May",
  journal = "IEEE Transactions on Computers",
  number =  "5",
  pages =   "443--464",
  title =   "{AQUILA}: {A}n equivalence checking system for large sequential designs",
  volume =  "49"
}

@inproceedings{StK97,
  author =  "D. Stoffel and W. Kunz",
  booktitle =   "Int'l Workshop on Logic \& Synthesis",
  year  =   "1997",
  month =   "May",
  title =   "A Structural Fixpoint Iteration For Sequential Logic Equivalence Checking Based on Retiming"
}

@inproceedings{GoPB00,
  author =  "E. Goldberg and M. R. Prasad and R. K. Brayton ",
  year  =   "2000",
  title =   "Using {SAT} in Combinational Equivalence Checking",
  month =   "May",
  booktitle =   "Int'l Workshop on Logic \& Synthesis",
}
@article{DoOf76,
  author =  "Donath, W.E. and Ofek, H.",
  year  =   "1976",
  journal = "IBM Technical Disclosure Bulletin",
  number =  "8",
  pages =   "2700--2703",
  title =   "Automatic Identification of Equivalence Points for {B}oolean Logic Verification",
  volume =  "18"
}

@inproceedings{Ber81,
  author =  "Berman, C.L.",
  booktitle =   "Proceedings of the 18th Design Automation Conference",
  year  =   "1981",
  month =   "June",
  pages =   "854--861",
  title =   "On Logic Comparison"
}

@inproceedings{GoDi98,
  author =  "Govindaraju, S.G. and Dill, D.L. and Hu, A.J. and Horowitz, M.A.",
  booktitle =   "Proceedings of the 35th Design Automation Conference",
  year  =   "1998",
  month =   "June",
  pages =   "451--455",
  title =   "Approximate reachability analysis with {BDD}s using overlapping projections"
}

@inproceedings{HuDi93,
  author =  "Hu, A.J. and Dill, D.L.",
  booktitle =   "Proceedings of the 30th Design Automation Conference",
  year  =   "1993",
  month =   "June",
  pages =   "266--271",
  title =   "Reducing {BDD} size by exploiting functional dependencies"
}

@inproceedings{EiJe96,
  author =  "C.A.J. van Eijk and J.A.G. Jess",
  booktitle =   "European Design \& Test Conference",
  year  =   "1996",
  month =   "March",
  pages =   "9--14",
  title =   "Exploiting Functional Dependencies in Finite State Machine Verification"
}

@article{LeWGH97,
  author =  "Eric Lehman and Yosinori Watanabe and Joel Grodstein and Heather Harkness",
  year  =   "1997",
  month =   "August",
  journal = "IEEE Transactions on Computer-Aided Design",
  number =  "8",
  pages =   "813--834",
  title =   "Logic Decomposition During Technology Mapping",
  volume =  "16"
}

@inproceedings{KuBa01,
  author =  "Andreas Kuehlmann and Jason Baumgartner",
  booktitle =   "Computer-Aided Verification",
  month =       "July",
  year  =   "2001",
  title =   "Transformation-Based Verification Using Generalized Retiming"
}


@inproceedings{MoSHK01,
  author =  "John Moondanos and Carl-Johans H. Seger and Ziyad Hanna and Daher Kaiss",
  booktitle =   "Computer-Aided Verification",
  month =       "July",
  year  =   "2001",
  pages =   "131--143",
  title =   "{CLEVER}: Divide and Conquer {C}ombinational {L}ogic {E}quivalence {VER}ification with False Negative Elimination"
}

@inproceedings{DoPiPo01,
  author =  "Agnostino Dovier and Carla Piazza and Alberto Polticriti",
  booktitle =   "Computer-Aided Verification",
  month =       "July",
  year  =   "2001",
  pages =   "79--90",
  title =   "A Fast Bisimulation Algorithm"
}

@inproceedings{ToKYT00,
  author =  "Masahiko Toyonaga and Keiichi Kurokawa and Takuya Yasui and Atsushi Takahashi",
  booktitle =   "Proceedings of the Int'l Symposium on Physical Design (ISPD'00)",
  year  =   "2000",
  month =   "April",
  title =   "A Practical Clock Tree Synthesis for Semi-Synchronous Circuits"
}

@inproceedings{LiPF99,
  author =  "Xun Liu and Marios C. Papaefthymiou and Eby G. Friedman",
  booktitle =   "Proceedings of the 36th Design Automation Conference",
  year  =   "1999",
  month =   "June",
  pages =   "321--236",
  title =   "Maximizing Performance by Retiming and Clock Skew Scheduling"
}

@inproceedings{AgJS99,
  author =  "Mark D. Aagaard and Robert B. Jones and Carl-Johans H. Seger",
  booktitle =   "Design Automation Conference",
  year  =   "1999",
  month =   "June",
  pages =   "402--407",
  title =   "Formal verification using parametric representations of {B}oolean constraints"
}

@article{Fis90,
  author =  "John P. Fishburn",
  year  =   "1990",
  month =   "July",
  journal = "IEEE Transactions on Computers",
  number =  "7",
  pages =   "945--951",
  title =   "Clock Skew Optimization",
  volume =  "39"
}

@inproceedings{Sar00,
  author =  "Thierry Sarrazin",
  booktitle =   "Proceedings of the {SAME2000} Conference",
  year  =   "2000",
  month =   "Oct.",
  pages =   "100--105",
  title =   "Clock Tree: The Quest For Zero Skew is Over"
}

@inproceedings{ShR94,
  author =      "N. Shenoy and R. Rudell",
  booktitle =   "Digest of Technical Papers of the Int'l Conference on Computer-Aided Design",
  year  =   "1994",
  month =   "Nov.",
  pages =       "226--233",
  title =       "Efficient Implementation of Retiming"
}
@inproceedings{RoAV97,
  author =  "James A. Rowson and Alberto Sangiovanni-Vincentelli",
  booktitle =   "Proceedings of the 34th Design Automation Conference",
  year  =   "1997",
  month =   "June",
  pages =   "178--183",
  title =   "Interface-Based Design"
}

@article{GrL65,
  author =  "A. Grasselli and F. Luccio",
  year  =   "1965",
  month =   "June",
  journal = "IEEE Trans. Elec. Comp.",
  pages =   "350--359",
  title =   "A Method for minimizing the number of internal states in incompletly specified sequential networks",
  volume =  "EC-14"
}

@article{HaO93,
  author =      "M. Hartmann and J. Orlin",
  title =       "Finding Minimum Cost to Time Ratio Cycles with Small Integral Transit Times",
  journal =     "Networks: {A}n Int'l Journal",
  volume =      "23",
  pages =   "567-574",
  year =        "1993"
}

@inproceedings{HaE97,
  author =  "Soha Hassoun and Carl Ebeling",
  booktitle =   "Int'l Workshop on Logic \& Synthesis",
  year  =   "1997",
  month =   "May",
  title =   "Sequential Circuit Optimization Using Precomputation"
}

@inproceedings{HaE96,
  author =  "Soha Hassoun and Carl Ebeling",
  booktitle =   "Design Automation Conference",
  year  =   "1996",
  month =   "June",
  pages =   "708--713",
  title =   "Architectural Retiming: Pipelining Latency-Constrained Circuits"
}

@inproceedings{HaEb98,
  author =  "Soha Hassoun and Carl Ebeling",
  booktitle =   "Int'l Conference on Computer-Aided Design",
  year  =   "1998",
  month =   "Nov.",
  pages =   "316--323",
  title =   "Using Precomputation in Architecture and Logic Synthesis"
}

@inproceedings{Ku98,
  author =  "David S. Kung",
  booktitle =   "Proceedings of the 35th Design Automation Conference",
  year  =   "1998",
  month =   "June",
  pages =   "352--355",
  title =   "A Fast Fanout Optimization Algorithm for Near-Continuous Buffer Libraries"
}

@inproceedings{SiSV90,
  author =  "K. J. Singh and Alberto Sangiovanni-Vincentelli",
  booktitle =   "Proceedings of the 27th Design Automation Conference",
  year  =   "1990",
  month =   "June",
  pages =   "357--360",
  title =   "A Heuristic Algorithm for the Fanout Problem"
}

@inproceedings{Gin90,
  author =  "Lukas {P.P.P. van Ginneken}",
  booktitle =   "Proceedings of the Int'l Symposium on Circuits and Systems",
  year  =   "1990",
  pages =   "865--868",
  title =   "Buffer Placement in Distributes {RC}-Tree Networks for Minimal {E}lmore Delay"
}

@book{KoFr00,
  author =  "Ivan S. Kourtev and Eby G. Friedman",
  year  =   "2000",
  publisher =   "Kluwer Academic Publisher",
  title =   "Timing Optimization through Clock Skew Scheduling"
}

@article{MaA98,
  author =      "Naresh Maheshwari and Sachin Sapatnekar",
  title =       "Efficient Retiming of Large Circuits",
  year  =   "1998",
  journal = "IEEE Transactions on Very Large Scale Integration",
  number =  "1",
  pages =   "74--82",
  volume =  "6"
}

@article{DeM91,
  author =  "Giovanni De Micheli",
  year  =   "1991",
  month =   "Jan.",
  journal = "IEEE Transactions on Computer-Aided Design",
  number =  "1",
  title =   "Synchronous Logic Synthesis: Algorithms for Cycle-Time Minimization",
  volume =  "10"
}


@article{WaGuBr96,
  author =  "Yosinori Watanabe and Lisa M. Guerra and Robert K. Brayton",
  year  =   "1996",
  month =   "July",
  journal = "IEEE Transactions on Computer-Aided Design",
  number =  "7",
  pages =   "734--744",
  title =   "Permissible Functions for Multioutput Components in Combinational Logic Optimization",
  volume =  "15"
}

@inproceedings{BiBJR97,
  author =  "G. P. Bischoff and K. S. Brace and S. Jain and R. Razdan",
  booktitle =   "Int'l Conference on Computer Design",
  year  =   "1997",
  month =   "Oct.",
  pages =   "16--24",
  title =   "Formal implementation verification of the bus interface unit for the {A}lpha 21264 microprocessor "
}

@inproceedings{YaD98,
  author =  "C. Han Yang and David L. Dill",
  booktitle =   "Design Automation Conference",
  year  =   "1998",
  month =   "June",
  pages =   "599--604",
  title =   "Validation with Guided Search of the State Space"
}

@inproceedings{YaD96,
  author =  "C. Han Yang and David L. Dill",
  booktitle =   "Int'l Workshop on High Level Design Validation and Test (HLDVT'96)",
  year  =   "1996",
  month =   "Nov.",
  title =   "SpotLight: Best-First Search of {FSM} State Space"
}

@inproceedings{HoSH00,
  author =  "Pei-Hsin Ho and Thomas Shiple and Kevin Harer and James Kukula and Robert Damiano and Valeria Bertacco and Jerry Taylor and Jiang Long",
  booktitle =   "Int'l Conference on Computer-Aided Design",
  year  =   "2000",
  month =   "Nov.",
  title =   "Smart Simulation Using Collaborative Formal and Simulation Engines"
}
%  pages =   "120--126",


@inproceedings{GaAK99,
  author =  "Malay Ganai and Adnan Aziz and Andreas Kuehlmann",
  booktitle =   "Design Automation Conference",
  year  =   "1999",
  month =   "June",
  pages =   "385--390",
  title =   "Enhancing Simulation with {BDD}s and {ATPG}"
}

@inproceedings{Ip00,
  author =  "C. Norris Ip",
  booktitle =   "Int'l Conference on Computer-Aided Design",
  year  =   "2000",
  month =   "Nov.",
  pages =   "127--133",
  title =   "Simulation Coverage Enhancement Using Stimulus Transformation"
}

@inproceedings{HaE97a,
  author =  "Soha Hassoun and Carl Ebeling",
  booktitle =   "Int'l Workshop on Timing Issues in the Specification and Synthesis of Digital Systems",
  year  =   "1997",
  month =   "Dec.",
  title =   "Experiments in the Iterative Application of Resynthesis and Retiming"
}

@inproceedings{GeBe94,
  author =  "Daniel Geist and Ilan Beer",
  booktitle =   "Computer-Aided Verification",
  year  =   "1994",
  month =   "July",
  pages =   "299--310",
  title =   "Efficient Model Checking by Automated Ordering of Transition Relation Partitions"
}

@inproceedings{Be+94,
  author =  "Ilan Beer and Shoham Ben-David and Daniel Geist and Ranaan Gewirtzman and Michael Yoeli",
  booktitle =   "Computer-Aided Verification",
  year  =   "1994",
  month =   "July",
  pages =   "182--193",
  title =   "Methodology and System for Practical Formal Verification of Reactive Hardware"
}

@inproceedings{RaA95,
  author =  "R. K. Ranjan and A. Aziz and R. K. Brayton and B. Plessier and C. Pixley",
  booktitle =   "Int'l Workshop on Logic \& Synthesis",
  year  =   "1995",
  month =   "June",
  title =   "Efficient {BDD} Algorithms for {FSM} Synthesis and Verification"
}

@inproceedings{MoKSS99,
  author =  "In-Ho Moon and James Kukula and Tom Shiple and Fabio Somenzi",
  booktitle =   "Digest of Technical Papers of the Int'l Conference on Computer-Aided Design",
  year  =   "1999",
  month =   "Nov.",
  pages =   "41--49",
  title =   "Least Fixpoint Approximations for Reachability Analysis"
}

@inproceedings{RaS95,
  author =  "Kavita Ravi and Fabio Somenzi",
  booktitle =   "Digest of Technical Papers of the Int'l Conference on Computer-Aided Design",
  year  =   "1995",
  month =   "Nov.",
  pages =   "154--158",
  title =   "High-Density reachability analysis"
}

@inproceedings{Ku01,
  author =  "Andreas Kuehlmann",
  booktitle =   "Proceedings of the Cadence Technical Conference",
  year  =   "2001",
  month =   "April",
  pages =   "1--6",
  title =   "A Survey of Sequential Circuit Optimization Techniques"
}

@INPROCEEDINGS {CaCQ96,
  ADDRESS =     "Santa Clara, CA" ,
  AUTHOR =      "G. Cabodi and P. Camurati and S. Quer",
  booktitle =   "Digest of Technical Papers of the Int'l Conference on Computer-Aided Design",
  MONTH =       "Nov.",
  PAGES =       "354-360" ,
  TITLE =       "Improved Reachability Analysis of Large Finite State Machines" ,
  YEAR =        "1996"
}

@inproceedings{BiCC99,
  author =  "Armin Biere and Alessandro Cimatti and Edmund M. Clarke and Yunshan Zhu",
  booktitle =   "Tools and Algorithms for Construction and Analysis of Systems",
  year  =   "1999",
  month =   "March",
  pages =   "193--207",
  title =   "Symbolic Model Checking without {BDD}s"
}

@book{Kur94,
  author =  "Robert P. Kurshan",
  year  =   "1994",
  publisher =   "Princeton University Press",
  title =   "Computer-Aided Verification of Coordinating Processes"
}

@book{Dan63,
  author =  "George~G.~Dantzig",
  year  =   "1963",
  publisher =   "Princeton University Press",
  title =   "Linear Programming and Extensions"
}

@book{NewEco02,
  editor =  "Dale W. Jorgenson and Charles W. Wessner",
  year  =   "2002",
  publisher =   "National Academies Press",
  title =   "Measuring and Sustaining the New Economy: Report of a Workshop"
}


@inproceedings{DeMo97,
  author =  "David Deharbe and Anamaria Martins Moreira",
  booktitle =   "Correct Hardware Design and Verification Methods",
  year  =   "1997",
  month =   "Oct.",
  pages =   "203--213",
  title =   "Using Induction and {BDD}s to Model Check Invariants"
}

@inproceedings{BiCRZ99,
  author =  "Armin Biere and Edmund M. Clarke and Richard Raimi and Yunshan Zhu",
  booktitle =   "Computer-Aided Verification",
  year  =   "1999",
  month =   "July",
  pages =   "60--71",
  title =   "Verifying Safety Properties of a {P}ower{PC} Microprocessor Using Symbolic Model Checking without {BDD}s"
}


@inproceedings{SiShSt00,
  author =  "Mary Sheeran and Satnam Singh and Gunnar Stalmarck",
  booktitle =   "Formal Methods in Computer-Aided Design",
  year  =   "2000",
  month =   "Nov.",
  pages =   "108--125",
  title =   "Checking Safety Properties Using Induction and a {SAT}-Solver"
}

@inproceedings{YaSAA97,
  author =  "Jun Yuan and Jian Shen and Jacob Abraham and Adnan Aziz",
  booktitle =   "Computer-Aided Verification",
  year  =   "1997",
  month =   "June",
  pages =   "376--387",
  title =   "On Combining Formal and Informal Verification"
}

@inproceedings{HoBr95,
  author =  "Ramin Hojati and Robert K. Brayton",
  booktitle =   "Computer-Aided Verification",
  year  =   "1995",
  month =   "July",
  title =   "Automatic Datapath Abstraction of Hardware Systems"
}

@inproceedings{dAHM00,
  author =  "Luca de Alfaro and Thomas A. Henzinger and Freddy Y. C. Mang",
  booktitle =   "Computer-Aided Verification",
  year  =   "2000",
  month =   "July",
  pages =   "186--201",
  title =   "Detecting Errors Before Reaching Them"
}


@inproceedings{HoBBM97,
  author =  "Youpyo Hong and Peter A. Beerel and Jerry R. Burch and Kenneth L. McMillan",
  booktitle =   "Design Automation Conference",
  year  =   "1997",
  month =   "June",
  pages =   "208--213",
  title =   "Safe {BDD} Minimization Using Don't Cares"
}

@phdthesis{Ga01,
  author =  "Malay Ganai",
  year  =   "2001",
  month =   "May",
  school =  "University of Texas",
  title =   "Algorithms for Efficient State Space Search"
}

@phdthesis{Ba02t,
  author =  "Jason Baumgartner",
  year  =   "2002",
  month =   "Dec.",
  school =  "University of Texas",
  title =   "Automatic Structural Abstraction Techniques for Enhanced Verification"
}

@inproceedings{WiBCG00,
  author =  "Poul F. Williams and Armin Biere and Edmund M. Clarke and Anubhav Gupta",
  booktitle =   "Computer-Aided Verification",
  year  =   "2000",
  month =   "July",
  pages =   "124--138",
  title =   "Combining Decision Diagrams and {SAT} Procedures for Efficient
 Symbolic Model Checking"
}

@inproceedings{MoGS00,
  author =  "In-Ho Moon and Gary D. Hachtel and Fabio Somenzi",
  booktitle =   "Formal Methods in Computer-Aided Design",
  year  =   "2000",
  month =   "Nov.",
  title =   "Border-block Triangular Form and Conjunction Schedule in Image Computation"
}
%  pages =   "73--90",

@inproceedings{BeGhAa00,
  author =  "Robert Beers and Rajnish Ghughal and Mark Aagaard",
  booktitle =   "Formal Methods in Computer-Aided Design",
  year  =   "2000",
  month =   "Nov.",
  title =   "Applications of Hierarchical Verification in Model Checking"
}




@inproceedings{Fi91,
  author =  "Thomas Filkorn",
  booktitle =   "Computer-Aided Verification",
  year  =   "1991",
  month =   "June",
  pages =   "225--232",
  title =   "Functional Extension of Symbolic Model Checking"
}

@article{ChHM96,
  author =      "H. Cho and Gary D. Hachtel and E. Macii and B. Pleisser and
                 Fabio Somenzi",
  year  =       "1996",
  month =       "Dec.",
  journal =     "IEEE Transactions on Computer-Aided Design",
  number =      "12",
  pages =       "1465--1478",
  title =       "Algorithms for Approximate {FSM} Traversal Based on
  State Space Decomposition",
  volume =      "15"
}



@book{network_flows,
  author =  "Ravindra K. Ahuja and Thomas L. Magnanti and James B. Orlin",
  year  =   "1993",
  publisher =   "Prentice-Hall, Inc.",
  title =   "Network Flows: Theory, Algorithms, and Applications"
}

@book{kohavi70,
  author =  "Zvi Kohavi",
  year  =   "1978",
  publisher =   "McGraw-Hill",
  title =   "Switching and Finite Automata Theory"
}

@book{milner89,
  author =  "Robin Milner",
  year  =   "1989",
  publisher =   "Prentice-Hall, Inc.",
  title =   "Communication and Concurrency"
}

@inproceedings{BK01,
  author =  "Jason Baumgartner and Andreas Kuehlmann",
  booktitle =   "Int'l Conference on Computer-Aided Design",
  year  =   "2001",
  month =   "Nov.",
  title =   "Min-Area Retiming on Flexible Circuit Structures"
}
%  pages =   "176--192",

@inproceedings{SiKB01,
  author =  "Subarnarekha Sinha and Andreas Kuehlmann and Robert K. Brayton",
  booktitle =   "Int'l Conference on Computer-Aided Design",
  year  =   "2001",
  month =   "Nov.",
  pages =   "84--90",
  title =   "Sequential {SPFD}s"
}



@inproceedings{BK01a,
  author =  "Jason Baumgartner and Andreas Kuehlmann",
  booktitle =   "Int'l Workshop on Logic \& Synthesis",
  year  =   "2001",
  month =   "Nov.",
  title =   "Min-Area Retiming on Flexible Circuit Structures"
}

@inproceedings{ClGr00,
  author =  "Edmund M. Clarke and Orna Grumburg and Somesh Jha and Yuan Lu and Helmut Veith",
  booktitle =   "Computer-Aided Verification",
  year  =   "2000",
  month =   "July",
  pages =   "154-169",
  title =   "Counterexample-Guided Abstraction Refinement"
}

@inproceedings{LNAn99,
  author =  "Jorn Lind-Nielsen, Henrik Reif Andersen",
  booktitle =   "Computer-Aided Verification",
  year  =   "1999",
  month =   "July",
  pages =   "8--17",
  title =   "Stepwise {CTL} Model Checking of State/Event Systems"
}

@inproceedings{HoCe00,
  author =  "Jin Hou and Eduard Cerny",
  booktitle =   "Formal Methods in Computer-Aided Design",
  year  =   "2000",
  month =   "Nov.",
  pages =   "299--315",
  title =   "Model Reductions and a Case Study"
}

@inproceedings{RFN01,
  author =  "Dong Wang and Pei-Hsin Ho and Jiang Long and James H. Kukula and Yunshan Zhu and Hi-Keung Tony Ma and Robert F. Damiano",
  booktitle =   "Proceedings of the 38th Design Automation Conference",
  year  =   "2001",
  month =   "June",
  pages =   "35--40",
  title =   "Formal Property Verification by Abstraction Refinement with Formal, Simulation and Hybrid Engines"
}


@article{BCG88,
  author =  "Michael C. Browne and Edmund M. Clarke and Orna Grumberg",
  year  =   "1988",
  publisher =   "Elsevier Science Publishers B.V.",
  journal = "Theoretical Computer Science",
  pages =   "115--131",
  title =   "Characterizing Finite {K}ripke Structures in Propositional Temporal Logic",
  volume =  "59"
}

@article{Em90,
  author =  "E. Allen Emerson",
  year  =   "1990",
  publisher =   "Elsevier Science Publishers B.V.",
  journal = "Handbook of Theoretical Computer Science",
  pages =   "996--1072",
  title =   "Temporal and Modal Logic",
  volume =  "B"
}


@article{EH86,
  author =  "E. Allen Emerson and Joseph Y. Halpern",
  year  =   "1986",
  publisher =   "Association for Computing Machinery",
  journal = "Journal of the ACM",
  number =      "1",
  pages =   "151--178",
  title =   "`{S}ometimes' and `Not never' revisited: on branching time versus linear time temporal logic",
  volume =  "33"
}

@article{FoFu56,
  author =  "L. R. Ford and D. R. Fulkerson",
  year  =   "1956",
  journal = "Canadian Journal of Mathematics",
  volume =      "8",
  pages =   "399--404",
  title =   "Maximal Flow Through a Network"

}


@article{GuLo94,
  author =  "Orna Grumberg and David E. Long",
  year  =   "1994",
  publisher =   "Association for Computing Machinery",
  journal = "ACM Transactions on Programming Languages and System",
  number =      "3",
  pages =   "843--871",
  title =   "Module Checking and Modular Verification",
  volume =  "16"
}


@inproceedings{Orlin88,
  author =  "James B. Orlin",
  booktitle =   "Proceedings of the 20th ACM Symposium on the Theory of
Computing",
  year  =   "1988",
  month =   "May",
  pages =   "377--387",
  title =   "A Faster Strongly Polynomial Minimum Cost Flow Algorithm"
}

@inproceedings{StMe73,
  author =  "L.~J.~Stockmeyer and A.~R.~Meyer",
  booktitle =   "Proceedings of the 5th ACM Symposium on the Theory of
Computing",
  year  =   "1973",
  month =   "April",
  pages =   "1--9",
  title =   "Word Problems Requiring Exponential Time"
}


@inproceedings{Cook71,
  author =  "S. A. Cook",
  booktitle =   "Proceedings of the 3rd ACM Symposium on the Theory of
Computing",
  year  =   "1971",
  month =   "May",
  pages =   "151--158",
  title =   "The Complexity of Theorem-Proving Procedures"
}

@inproceedings{HeQaRa99,
  author =  "Thomas A. Henzinger and Shaz Qadeer and Sriram K. Rajamani",
  booktitle =   "Computer-Aided Verification",
  year  =   "1999",
  month =   "July",
  pages =   "208--221",
  title =   "Assume-guarantee Refinement Between Different Time Scales"
}

@inproceedings{AlHu01,
  author =  "Alvin R. Albrecht and Alan J. Hu",
  booktitle =   "Correct Hardware Design and Verification Methods",
  year  =   "2001",
  month =   "Sept.",
  pages =   "126--139",
  title =   "Register Transformations with Multiple Clock Domains"
}


@article{chma89,
  author =  "Joseph Cheriyan and Sanjay N. Maheshwari",
  year  =   "1989",
  publisher =   "Society for Industrial and Applied Mathematics",
  journal = "SIAM Journal on Computing",
  number =      "6",
  pages =   "1057--1086",
  title =   "Analysis of Preflow Push Algorithms for Maximum Network Flow",
  volume =  "18"
}

@inproceedings{sug01,
  author =  "Ilan Beer and Shohan Ben-David and Cindy Eisner and Dana Fisman and Anna Gringauze and Yoav Rodeh",
  booktitle =   "Computer-Aided Verification",
  month =       "July",
  year  =   "2001",
  pages =   "363--367",
  title =   "The Temporal Logic {\em Sugar}"
}


@inproceedings{beer96,
  author =  "Ilan Beer and Shohan Ben-David and Cindy Eisner and Avner Landver",
  booktitle =   "Design Automation Conference",
  year  =   "1996",
  month =   "June",
  pages =   "655--660",
  title =   "Rule{B}ase: an Industry-Oriented Formal Verification Tool"
}

@inproceedings{AzSSS94,
    author = "Adnan Aziz and Thomas R. Shiple and Vigyan Singhal and Alberto L. Sangiovanni-Vincentelli",
    title = "Formula-Dependent Equivalence for Compositional {CTL} Model Checking",
    booktitle = "Computer-Aided Verification",
    pages = "324--337",
    month = "June",
    year = "1994"
}



@inproceedings{hu94,
  author =  "Alan J. Hu and Gary York and David L. Dill",
  booktitle =   "Design Automation Conference",
  year  =   "1994",
  month =   "June",
  pages =   "276--282",
  title =   "New Techniques for Efficient Verification with Implicitly Conjoined {BDD}s"
}



@inproceedings{jiku02,
  author =  "HoonSang Jin and Andreas Kuehlmann and Fabio Somenzi",
  booktitle =   "Tools and Algorithms for the Construction and Analysis of Systems",
  year  =   "2002",
  month =   "April",
  pages =   "312--326",
  title =   "Fine-Grain Conjunction Scheduling for Symbolic Reachability Analysis"
}

@inproceedings{ClEm81,
  author =  "Edmund M. Clarke and E. Allen Emerson",
  booktitle =   "Proceedings of the Workshop on Logic of Programs",
  year  =   "1981",
  month =   "May",
  pages =   "52--71",
  title =   "Design and synthesis of synchronization skeletons using branching-time temporal logic"
}

@inproceedings{GePVW95,
  author =  "Rob Gerth and Doron Peled and Moshe Y. Vardi and Pierre Wolper",
  booktitle =   "Protocol Specification Testing and Verification",
  year  =   "1995",
  month =   "June",
  pages =   "3--18",
  title =   "Simple On-the-fly automatic verification of linear temporal logic"
}

@inproceedings{YeChJo02,
  author =  "Chia-Chih Yen and Kuang-Chien Chen and Jing-Yang Jou",
  booktitle =   "Int'l Workshop on Logic \& Synthesis",
  year  =   "2002",
  pages =   "149--154",
  title =   "A Practical Approach to Cycle Bound Estimation"
}
%  month =  "June",


@inproceedings{BaKuAb02,
  author =  "Jason Baumgartner and Andreas Kuehlmann and Jacob Abraham",
  booktitle =   "Computer-Aided Verification",
  month =       "July",
  year  =   "2002",
  title =   "Property Checking via Structural Analysis"
}
%  pages =   "151--165",


@inproceedings{McM02,
  author =  "Ken L. McMillan",
  booktitle =   "Computer-Aided Verification",
  month =       "July",
  year  =   "2002",
  pages =   "250--264",
  title =   "Applying {SAT} Methods in Unbounded Symbolic Model Checking"
}


@phdthesis{Ra97,
  author =  "Rajeev K. Ranjan",
  year  =   "1997",
  month =   "Dec.",
  school =  "University of California at Berkeley",
  title =   "Design and Implementation Verification of Finite State Systems"
}


@inproceedings{MoKuRaSi00,
  author =  "In-Ho Moon and James H. Kukula and Kavita Ravi and Fabio Somenzi",
  booktitle =   "Design Automation Conference",
  year  =   "2000",
  month =   "June",
  pages =   "23--28",
  title =   "To Split or to Conjoin: the Question in Image Computation"
}

@article{LeTa79,
  author =  "T. Lenguaer and Robert E. Tarjan",
  year  =   "1970",
  month =   "July",
  journal = "Transactions of Programming Languages and Systems",
  pages =   "121--141",
  title =   "A Fast Algorithm for Finding Dominators in a Flowgraph",
}

@inproceedings{BeBeLa98,
  author =  "Ilan Beer and Shoham Ben-David and Avner Landver",
  booktitle =   "Computer-Aided Verification",
  year  =   "1998",
  month =   "July",
  pages =   "184--194",
  title =   "On-the-fly model checking of {RCTL} formulas"
}


@inproceedings{WiDiBr00,
  author =  "Chris Wilson and David L. Dill and Randal E. Bryant",
  booktitle =   "Formal Methods in Computer-Aided Design",
  year  =   "2000",
  month =   "Nov.",
  pages =   "335--353",
  title =   "Symbolic Simulation with Approximate Values"
}


@inproceedings{WiDi00,
  author =  "Chris Wilson and David L. Dill",
  booktitle =   "Proceedings of the 37th Design Automation Conference",
  year  =   "2000",
  month =   "June",
  pages =   "124--129",
  title =   "Reliable verification using symbolic simulation with scalar values"
}


@inproceedings{BiHu02,
  author =  "Jesse D. Bingham and Alan J. Hu",
  booktitle =   "Computer-Aided Verification",
  month =       "July",
  year  =   "2002",
  pages =   "280--294",
  title =   "Semi-formal bounded model checking"
}

@inproceedings{StKu97a,
  author =  "Dominik Stoffel and Wolfgang Kunz",
  booktitle =   "Int'l Conference on Computer-Aided Design",
  year  =   "1997",
  month =   "Nov.",
  pages =   "9--13",
  title =   "Record & Play: A Structural Fixed Point Iteration for Sequential Circuit Verification"
}


@inproceedings{GaAz99,
  author =  "Malay Ganai and Adnan Aziz",
  booktitle =   "Int'l Workshop on High Level Design Validation and Test (HLDVT'99)",
  year  =   "1999",
  month =   "Nov.",
  title =   "Enhancements to Invariant Verification using {SIVA}"
}

@inproceedings{CaCaQu02,
  author =  "Gianpiero Cabodi and Paolo E. Camurati and Stefano Quer",
  booktitle =   "Design Automation Conference",
  year  =   "2002",
  month =   "June",
  pages =   "117--122",
  title =   "Can {BDD}s Compete with {SAT} Solvers on Bounded Model Checking?"
}


@inproceedings{BeOl02,
  author =  "Valeria Bertacco and Kunle Olukotun",
  booktitle =   "Design Automation Conference",
  year  =   "2002",
  month =   "June",
  pages =   "99--104",
  title =   "Efficient State Representation for Symbolic Simulation"
}


@article{Moore65,
  author =  "Gordon E. Moore",
  month =   "April",
  year  =   "1965",
  journal = "Electronics",
  number =  "8",
  volume =  "38",
  pages =   "114--117",
  title =   "Cramming More Components Onto Integrated Circuits"
}

@article{PaDi80,
  author =  "D.~A.~Patterson and D.~R.~Ditzel",
  month =   "Oct.",
  year  =   "1980",
  journal = "Computer Architecture News",
  number =  "6",
  volume =  "8",
  pages =   "25--33",
  title =   "The Case for the Reduced Instruction Set Computer"
}


@article{GeGaPaYu89,
  author =  "Patrick Gelsinger and Paolo Gargini and Gerhard Parker and Albert Yu",
  year  =   "1989",
  month =   "Oct.",
  journal = "IEEE Spectrum",
  number =  "10",
  volume =  "26",
  pages =   "43--47",
  title =   "Microprocessors circa 2000"
}


@techreport{AzSiBr93,
  author =  "Adnan Aziz and Vigyan Singhal and Robert K. Brayton",
  year  =   "1993",
  month =   "July",
  number =  "UCB/ERL M93/52",
  institution = "University of California at Berkeley",
  title =   "Verifying Interacting Finite State Machines: Complexity Issues"
}


%and W.~Roesner and G.~M.~Heiling and J.~R.~Reysa and J.~R.~Jackson and B.-L.~Chu and M.~L.~Behm and J.~Baumgartner and R.~D.~Peterson and J.~Abdulhafiz and W.~E.~Bucy and J.~H.~Klaus and D.~J.~Klema and T.~N.~Le and F.~D.~Lewis and P.~E.~Milling and L.~A.~McConville and B.~S.~Nelson and V.~Paruthi and T.~W.~Pouarz and A.~D.~Romonosky and J.~Stuecheli and K.~D.~Thompson and D.~W.~Victor and B.~Wile",
@article{Power4_02,
  author = "{J.~M.~Ludden et al.}",
  year  =   "2002",
  month =   "Jan.",
  journal = "IBM Journal of Research and Development",
  number =  "1",
  title =   "Functional verification of the {POWER4} microprocessor and {POWER4} multiprocessor systems",
  volume =  "46"
}
%  pages =  "53--76",


@article{Ga+01,
  author =  "Malay Ganai, Praveen Yalagandula, Adnan Aziz, Andreas Kuehlmann and Vigyan Singhal",
  year  =   "2001",
  month =       "February",
  journal = "Journal of Electronic Testing: Theory and Applications",
  pages =   "123--144",
  volume =  "F13",
  title =   "SIVA: A System for Coverage Directed State Space Search"
}

@inproceedings{YaSA00,
  author =  "Praveen Yalagandula and Vigyan Singhal and Adnan Aziz",
  booktitle =   "Design, Automation, and Test in Europe",
  year  =   "2000",
  month =   "March",
  pages =   "237--242",
  title =   "Automatic lighthouse generation for directed state space search"
}


@article{Pn84,
  author =  "Amir Pnueli",
  year  =   "1985",
  publisher =   "{NATO} {ASI} Series",
  journal = "Logics and Models of Concurrent Systems",
  pages =   "123--144",
  title =   "In transition from global to modular temporal reasoning about programs",
  volume =  "F13"
}

@inproceedings{ClGrLo92,
  author =  "Edmund M. Clarke and Orna Grumberg and David E. Long",
  booktitle =   "Symposium on the Principles of Programming Languages",
  year  =   "1992",
  month =   "Jan.",
  pages =   "343--354",
  title =   "Model Checking and Abstraction"
}


@inproceedings{CoCo77,
  author =  "P. Cousot and R. Cousot",
  booktitle =   "ACM Symposium on the Principles of
Programming Languages",
  year  =   "1977",
  month =   "Jan.",
  pages =   "238--252",
  title =   "Abstract Interpretation: A Unified Lattice Model
for Static Analysis of Programs by Construction or Approximation of Fixpoints"
}



@Article{DGG97,
  author =       "Dannis Dams and Rob Gerth and Orna Grumberg",
  title =        "Abstract Interpretation of Reactive Systems",
  journal =      "{ACM} Transactions on Programming Languages and Systems",
  year =         "1997",
  volume =       "19",
  number =       "2",
  pages  =       "253--291"
}


@inproceedings{HoIsKiBr95,
  author =  "Ramin Hojati and Adrian Isles and Desmond Kirkpatrick and Robert Brayton",
  booktitle =   "Formal Methods in Computer-Aided Design",
  year  =   "1996",
  month =   "Nov.",
  title =   "Verification Using Uninterpreted Functions and Finite Instantiations"
}
%  pages =  "218--232",

@inproceedings{HoIsKa98,
  author =  "Pei-Hsin Ho and Adrian J. Isles and Timothy Kam",
  booktitle =   "Int'l Conference on Computer-Aided Design",
  year  =   "1998",
  month =   "Nov.",
  pages =   "529--536",
  title =   "Formal Verification of Pipeline Control Using Controlled Token Nets and Abstract Interpretation"
}



@inproceedings{PaMaVe98,
  author =  "Viresh Paruthi and Nazanin Mansouri and Ranga Vemuri",
  booktitle =   "Int'l Conference on Computer Design",
  year  =   "1998",
  month =   "Oct.",
  pages =   "192--194",
  title =   "Automatic Data Path Abstraction for Verification of Large Scale Designs"
}


@inproceedings{MaHoRb98,
 author = "Gurmeet Singh Manku and Ramin Hojati and Robert K. Brayton",
 title = "Structural Symmetry and Model Checking",
 pages = "159--171",
 booktitle =    "Computer-Aided Verification",
 year = "1998",
 month =    "July",
}


@inproceedings{IpDi93,
    author = "C. Norris Ip and David L. Dill",
    title = "Better Verification Through Symmetry",
    booktitle = "Computer Hardware Description Languages and their Applications",
    pages = "97--111",
    year = "1993"
}


@inproceedings{EmSi93,
  author = "E. Allen Emerson and A. Prasad Sistla",
  title =     "Symmetry and Model Checking",
  year =      "1993",
  booktitle = "Computer Aided Verification",
  pages = "463--478"
}

@inproceedings{sis-iccd,
  author = "E.~M.~Sentovich and K.~J.~Singh and C.~Moon and H.~Savoj
                and R.~K.~Brayton and A.~L.~Sangiovanni-Vincentelli",
  title = "Sequential Circuit Design Using Synthesis and Optimization",
  booktitle =   "Int'l Conference on Computer Design",
  pages = "328--333",
  month = "Oct.",
  year = "1992"
}

@InCollection{ImmermanTCDecidability04,
  author = "N. Immerman and A. Rabinovich and T.  Reps and S. Sagiv and G. Yorsh",
  title = "The boundary between decidability and undecidability for transitive-closure logics",
  year="2004",
  booktitle="Computer Science Logic",
}

@InCollection{srivas:hw-pvs,
  title =        "Hardware Verification Using {PVS}",
  author =       "Mandayam Srivas and Harald Rue{\ss} and David Cyrluk",
  booktitle =    "Formal Hardware Verification: Methods and Systems in
                 Comparison",
  pages =        "156--205",
  year =         "1997",
  publisher =    "Springer-Verlag",
}

%  series =       "Lecture Notes in Computer Science",
%  volume =       "1287",
%  editor =       "Thomas Kropf",


@book{KaMM00,
  author = "Matt Kaufmann and Panagiotis Manolios and J Strother Moore",
  publisher = "Kluwer Academic Publishers",
  year  =   "2000",
  title =   "Computer-Aided Reasoning: An Approach"
}

@inproceedings{zhma02,
  author =  "Lintao Zhang and Sharad Malik",
  booktitle =   "Int'l Conference on Computer Design",
  year  =   "2002",
  month =   "Nov.",
  pages =   "442--449",
  title =   "Conflict Driven Learning in a Quantified {B}oolean Satisfiability Solver"
}

@inproceedings{KS03,
  author    = "Daniel Kroening and Ofer Strichman",
  title     = "Efficient Computation of Recurrence Diameters",
  booktitle = "Int'l Conference on Verification, Model Checking, and Abstract Interpretation",
  year      = "2003",
  pages     = "298--309",
  month     = "Jan.",
}

@inproceedings{vE98,
  author =  "C. A. J. van Eijk",
  booktitle =   "Design, Automation, and Test in Europe",
  year  =   "1998",
  month =   "March",
  pages =   "618--623",
  title =   "Sequential equivalence checking without state space traversal"
}

@article{RabinS2S69, 
  author="Michael O. Rabin",
  title="Decidability of Second-order theories and automata on infinite trees",
  year=1969,
  journal="Transactions of the American Mathematical Society",
}

@article{GrLo94,
  author =  "Orna Grumberg and David E. Long",
  year  =   "1994",
  publisher =   "Association for Computing Machinery",
  journal = "ACM Transactions on Programming Languages and System",
  title =   "Model Checking and Modular Verification",
  volume =  "16(3)"
}

@phdthesis{Wang03,
  author =      "Dong Wang",
  school =      "Carnegie Mellon University",
  year  =       "2003",
  month =       "May",
  title =       "{SAT} based Abstraction Refinement for Hardware Verification"
}

@phdthesis{Isles00,
  author =      "Adrian Isles",
  school =      "University of California at Berkeley",
  year  =       "2000",
  month =       "May",
  title =       "Formal Verification using Datapath Abstraction"
}

@inproceedings{AndrausSakallah2004,
    author = {Z. S. Andraus and K. A. Sakallah},
    title = {Automatic Abstraction and Verification of {V}erilog
              Models},
    booktitle =  {Design Automation Conference},
    month = {June},
    year = {2004}
}
%    pages = {218-223},

@inproceedings{IsHB98,
 author = "Adrian Isles and Ramin Hojati and Robert Brayton",
 title = "Computing Reachable Control States of Systems Modeled with Uninterpreted Functions and Infinite Memory",
 booktitle =    "Computer-Aided Verification",
 year = "1998",
}
% month =   "July",
% pages = "256--267",

@inproceedings{HoIK98,
  author =  "Pei-Hsin Ho and Adrian J. Isles and Timothy Kam",
  booktitle =   "Int'l Conference on Computer-Aided Design",
  year  =   "1998",
  month =   "Nov.",
  title =   "Formal verification of pipeline control using controlled token nets and abstract interpretation"
}
%  pages =  "529--536",


@inproceedings{ zhou98how,
  author = "H. Zhou and V. Singhal and A. Aziz",
  title = "How Powerful is Retiming?",
  booktitle =   "Int'l Workshop on Logic \& Synthesis",
  year = "1998",
  month =   "May"
}

@Article{Alp98,
  author =  "Charles Alpert and Jen-Hsin Huang and Andrew Kahng",
  year  =   "1998",
  journal = "IEEE Transactions on Computer-Aided Design",
  number =      "17",
  volume =      "8",
  title =   "Multilevel Circuit Partitioning",
  pages =   "655--667"
}

%book{IbmFv,
%  author =  "{IBM Formal Verification Benchmark Library}",
%  year  =   "",
%  publisher =   "http://www.haifa.il.ibm.com/{\\}projects/verification/RB\_Homepage/fvbenchmarks.html",
%  title =   ""
%}

@inproceedings{BjBo04,
  author =  "Per Bjesse and Arne Boralv",
  booktitle =   "Int'l Conference on Computer-Aided Design",
  year  =   "2004",
  month =   "Nov.",
  title =   "{DAG}-Aware Circuit Compression For Formal Verification"
}

@book{minisatid08,
    author = {Maarten Marien and Johan Wittocx and Marc Denecker and Maurice Bruynooghe},
    title={SAT(ID): Satisfiability for propositional logic with inductive definitions},
    booktitle={Hans Kleine B�uning and Xishun Zhao, editors, SAT, volume 4996 of LCNS},
    year={2008},
    publisher={Springer},
}

@book{bbook96,
    author = "Jean-Raymond Abrial",
    title = "The B-Book: Assigning Programs to Meanings",
    publisher = "Cambridge University Press",
    year="1996",
}

@book{sem96,
    author = "H. Zhang and J. Zhang",
    title="Generating models by SEM",
    booktitle="International Conference on Automated Deduction",
    year="1996",
    publisher={Springer-Verlag},
}

@inproceedings{jpfinder,
    title="Java PathFinder webpage",
    url="http://javapathfinder.sourceforge.net"
}

@book{ocl99,
    author = "Jos Warmer and Anneke Kelppe",
    title = "The object constraint language: precise modeling with UML",
    year = "1999",
    publisher = "Addison-Wesley",
}

@inproceedings{idp2006,
    author="Maarten Marien and Johan Wittocx and Marc Denecker",
    title="The IDP framework for declarative problem solving",
    editors="E. Giunchiglia, V. Marek, D. Mitchell, and E. Ternovska",
    booktitle="Search and Logic: Answer Set Programming and SAT",
    pages="19-34", 
    year="2006",
}

@inproceedings{mace94,
    author = "W. McCune",
    title="A Davis-Putnam program and its application to finite first-order model: Quasigroup existence problems",
    booktitle=" Technical report, Argonne National Laboratory",
    year="1994",
}


@inproceedings{mace2008,
    author = "William McCune",
    title="Prover9 and MACE4",
    month="June",
    year="2008",
    url="http://www.cs.unm.edu/mccune/prover9/",
}

@inproceedings{darwinfm2007,
    author = "Peter Baumgartner and Alexander Fuchs and Hans de Nivelle and Cesare Tinelli",
    title="Computing finite models by reduction to function-free clause logic",
    booktitle="Journal of Applied Logic",
    year="2007"
}

@inproceedings{paradox2003,
    author = "Koen Claessen and Niklas Sorensson",
    title="New techniques that improve MACE-style finite model finding",
    booktitle="CADE-19 Workshop on Model Computation", 
    month="July",
    year="2003",
}


@inproceedings{znotation1992,
    author = "J. Michael Spivey",
    title = "The Z Notation: A reference manual",
    booktitle = "International series in computer science",
    year = "1992",
    publisher = "Prentice Hall",
}


@inproceedings{emerson99from,
    author = "E. Allen Emerson and Richard J. Trefler",
    title = "From Asymmetry to Full Symmetry: New Techniques for Symmetry Reduction in Model Checking",
    booktitle = "Correct Hardware Design and Verification Methods",
    year = "1999",
    url = "citeseer.ist.psu.edu/emerson99from.html" 
}

@inproceedings{chaff-dac-01,
        author = {Matthew W. Moskewicz and Conor F. Madigan and Ying Zhao and Lintao Zhang and and Sharad Malik},
        title = "{CHAFF: Engineering an Efficient SAT Solver.}",
        booktitle = dac,
        year = 2001
}
@inproceedings{aziz94e,
        author = { A. Aziz and V. Singhal and G. Swamy and R. Brayton},
        title = "{Minimizing Interacting Finite State Machines: A Compositional
                  Approach to Language Containment}",
        booktitle = iccd,
        pages = {255-261},
        month = oct,
        year = 1994
}
@article{aziz-fmsd-00,
        author = {A. Aziz and T. Shiple and V. Singhal and R. Brayton and
                  A. Sangiovanni-Vincentelli},
        title = "{Formula Dependent Equivalence for Compositional
                CTL Model Checking}",
        journal = fmsd,
        year = 2002,
        volume = 21,
        number = 2,
        pages = {193-224},
}
@book{hopcroft79,
  author = {J. Hopcroft and J. Ullman},
  title = "{Introduction to Automata Theory, Languages and Computation}",
  publisher = "Addison-Wesley",
  year = 1979
}
@inproceedings{brayton82,
        author = {R. K. Brayton and C. McMullen},
        title = "{The Decomposition and Factorization of Boolean Expressions}",
        booktitle = iscas,
        month = may,
        year = 1982
}
%         pages = {49-54},

@inproceedings{saldanha89,
        author = {A. Saldanha and A. R. Wang and R. K. Brayton and
                  A. L. Sangiovanni-Vincentelli},
        title = "{Multi-Level Logic Simplification using Don't Cares
                 and Filters}",
        booktitle = dac,
        pages = {277-282},
        year = 1989
}

@article{aziz-s1s-tcad-00,
    author = {A. Aziz and F. Balarin and R. Brayton and A. Sangiovanni-Vincentelli},
    title = "{Sequential Synthesis Using {\tt S1S}}",
    journal = ieeetcad,
    year = 2000,
    month = oct
}

@book{ansiC99standard,
  author = "{International Organization for Standardization}",
  title =   "ISO/IEC 9899:1999: Programming languages---C",
  institution= "International Organization for Standardization",
  year  =   "1999",
}

@book{IbmFv,
  author =  "{IBM Formal Verification Benchmark Library}",
  title =   " ",
  year  =   "",
  publisher = "http://www.haifa.il.ibm.com/{\\}projects/verification/RB\_Homepage/fvbenchmarks.html",
}
%%%%%%%%%%%%%%%%%%%kassem added the below papers to the database of Dr. Zaraket
@article{doESE05,
    author    = {Hyunsook Do and
                Sebastian G. Elbaum and
                Gregg Rothermel},
    title     = {Supporting Controlled Experimentation with Testing Techniques:
                An Infrastructure and its Potential Impact.},
    journal   = {Empirical Software Engineering: An International Journal},
    volume    = {10},
    number    = {4},
    pages     = {405--435},
    year      = {2005},
}

@article{gotlieb,
    author    = {Arnaud Gotlieb},
    title     = {TCAS software verification using Constraint Programming},
    journal   = {The Knowledge Engineering Review},
    volume    = {0},
    number    = {0},
    pages     = {1--15},
    year      = {2009},
}

@inproceedings{503230,
 author = {Coen-Porisini, Alberto and Denaro, Giovanni and Ghezzi, Carlo and Pezz\'{e}, Mauro},
 title = {Using symbolic execution for verifying safety-critical systems},
 booktitle = {Proceedings of the 8th European software engineering conference},
 year = {2001},
 isbn = {1-58113-390-1},
 location = {Vienna, Austria},
 }

@inproceedings{atac_2009,
 author = {Namin, Akbar Siami and Andrews, James H.},
 title = {The influence of size and coverage on test suite effectiveness},
 booktitle = {ISSTA '09: Proceedings of the eighteenth international symposium on Software testing and analysis},
 year = {2009},
 isbn = {978-1-60558-338-9},
 pages = {57--68},
 location = {Chicago, IL, USA},
 doi = {http://doi.acm.org/10.1145/1572272.1572280},
 }

@INPROCEEDINGS{atac, 
author={Horgan, J.R. and London, S.}, 
journal={Assessment of Quality Software Development Tools, 1992., Proceedings of the Second Symposium on}, title={A data flow coverage testing tool for C}, 
year={1992}, 
month={may.}, 
volume={}, 
number={}, 
pages={2 -10}, 
ISSN={},}

@inbook{tcas_manual,
  author =  "U.S. Department of Transportation Federal Aviation Administration",
  year  =   "2000",
  title =   "Introduction to TCAS II Version 7"
}

@inproceedings{pbcov,
 author = {Zaraket, Fadi and Masri, Wes},
 title = {Property based coverage criterion},
 booktitle = {DEFECTS '09: Proceedings of the 2nd International Workshop on Defects in Large Software Systems},
 year = {2009},
 isbn = {978-1-60558-654-0},
 pages = {27--28},
 location = {Chicago, Illinois},
 doi = {http://doi.acm.org/10.1145/1555860.1555870},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@inproceedings{crest,
 author = {Burnim, J. and Sen, K.},
 title = {Heuristics for Scalable Dynamic Test Generation},
 booktitle = {ASE '08: Proceedings of the 2008 23rd IEEE/ACM International Conference on Automated Software Engineering},
 year = {2008},
 isbn = {978-1-4244-2187-9},
 pages = {443--446},
 doi = {http://dx.doi.org/10.1109/ASE.2008.69},
 }

@conference{yices,
  title={{A fast linear-arithmetic solver for DPLL (T)}},
  author={Dutertre, B. and De Moura, L.},
  booktitle={Computer Aided Verification},
  pages={81--94},
  year={2006},
  organization={Springer}
}

@misc{ABC,
  author =  {Berkeley Logic Synthesis and Verification Group},
  title =   {ABC: A System for Sequential Synthesis and Verification  Release 70930},
  ftp =     {http://www.eecs.berkeley.edu/~alanmi/abc/},
}

@article{path,
  title={{Structured testing: A testing methodology using the cyclomatic complexity metric}},
  author={Watson, A.H. and McCabe, T.J. and Wallace, D.R.},
  journal={NIST Special Publication},
  volume={500},
  pages={235},
  year={1996}
}

@conference{infer,
  title={{Dynamically inferring temporal properties}},
  author={Yang, J. and Evans, D.},
  booktitle={Proceedings of the 5th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering},
  pages={23--28},
  year={2004},
  organization={ACM}
}

@inproceedings{cil,
 author = {Necula, George C. and McPeak, Scott and Rahul, Shree Prakash and Weimer, Westley},
 title = {CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs},
 booktitle = {Proceedings of the 11th International Conference on Compiler Construction},
 year = {2002},
 isbn = {3-540-43369-4},
 address = {London, UK},
 }

@ARTICLE{ammanSpecCov, 
author={Paul E. Ammann and Paul E. Black}, 
journal={International Journal of Reliability, Quality and Safety Engineering}, 
title={Specification-Based Coverage Metric to Evaluate Test Sets}, 
year={2001}, 
month={Dec}, 
volume={8}, 
number={4}, 
keywords={}, 
}

@article{mutation,
 author = {DeMillo, R. A. and Lipton, R. J. and Sayward, F. G.},
 title = {Hints on Test Data Selection: Help for the Practicing Programmer},
 journal = {Computer},
 volume = {11},
 number = {4},
 year = {1978},
 issn = {0018-9162},
 pages = {34--41},
 doi = {http://dx.doi.org/10.1109/C-M.1978.218136},
 publisher = {IEEE Computer Society Press},
 address = {Los Alamitos, CA, USA},
 }

@article{SMV,
  title={{The SMV system}},
  author={McMillan, K.L.},
  journal={Cadence Berkeley Labs},
  year={1999}
}

@book{gcov,
  author = "Brian J. Gough and Richard M. Stallman",
  title = "An Introduction to GCC",
  publisher = "Network Theory Ltd",
  year = "2005",
  month = "August",
}
%%%%%%%%%%%%%%%%%%%END KASSEM ADDED PAPERS%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
